Smart Contracts: From Formal Specification to Blockchain Code

Abstract

The combination of the Internet of Things (IoT), a type of Cyber Physical Systems (CPS), with Distributed Ledger Technology (DLT) platforms, also known as blockchains, provides an unprecedented opportunity for automating smart contracts that monitor the execution of legal contracts to ensure compliance. The absence of formalization of smart contracts based on recognized legal notions may however result in uncertainty during contract monitoring. The need for formal smart contract specifications, together with refinements and transformations to DLT implementations (code), is undeniable and urgent. This thesis, following a Design Science Research methodology, aims to partially address this need by developing a formal contract specification language called Symboleo, and selecting the suitable target language for generating smart contract code from Symboleo specifications. This thesis contributes a syntax and axiomatic semantics for Symboleo, with concepts rooted in a legal ontology, and supported by an editor. It also provides an analysis of possible target smart contract programming languages. These artifacts are evaluated with a comprehensive example of sales of perishable goods, with positive results.