Contracts are legally binding and enforceable agreements among two or more parties that govern social interactions. They have been used for millennia, including in commercial transactions, employment relationships and intellectual property generation. Each contract determines obligations and powers of contracting parties. The execution of a contract needs to be continuously monitored to ensure compliance with its terms and conditions. Smart contracts are software systems that monitor and control the execution of contracts to ensure compliance. But for such software systems to become possible, contracts need to be specified precisely to eliminate ambiguities, contradictions, and missing clauses. This thesis proposes a formal specification language for contracts named Symboleo. The ontology of Symboleo is founded on the legal concepts of obligation (a kind of duty) and power (a kind of right) complemented with the concepts of event and situation that are suitable for conceptualizing monitoring tasks. The formal semantics of legal concepts is defined in terms of state machines that describe the lifetimes of contracts, obligations, and powers, as well as axioms that describe precisely state transitions. The language supports execution-time operations that enable subcontracting assignment of rights and substitution of performance to a third party during the execution of a contract. Symboleo has been applied to the formalization of contracts from three different domains as a preliminary evaluation of its expressiveness. Formal specifications can be algorithmically analyzed to ensure that they satisfy desired properties. Towards this end, the thesis presents two implemented analysis tools. One is a conformance checking tool (SymboleoPC) that ensures that a specification is consistent with the expectations of contracting parties. Expectations are defined for this tool in terms of scenarios (sequences of events) and the expected final outcome (i.e., successful/unsuccessful execution). The other tool (SymboleoPC), which builds on top of an existing model checker (nuXmv), can prove/disprove desired properties of a contract, expressed in temporal logic. These tools have been used for assessing different business contracts. SymboleoPC is also assessed in terms of performance and scalability, with positive results. Symboleo, together with its associated tools, is envisioned as an enabler for the formal verification of contracts to address requirements-level issues, at design time.

In this dissertation, we address the problem of vagueness in traditional legal contracts by presenting novel methodologies that aid in the paradigm shift from traditional legal contracts to smart contracts. We discuss key enabling technologies that assist in converting the traditional natural language legal contract, which is full of vague words, phrases, and sentences to the blockchain-based precise smart contract, including metrics evaluation during our conversion experiment. To address the challenge of this contract-transformation process, we propose four novel proof-of-concept approaches that take vagueness and different possible interpretations into significant consideration, where we experiment with popular vendors' existing vague legal contracts. We show through experiments that our proposed methodologies are able to study the degree of vagueness in every interpretation and demonstrate which vendor's translated-smart contract can be more accurate, optimized, and have a lesser degree of vagueness. We also incorporated the method of fuzzy logic inside the blockchain-based smart contract, to successfully model the semantics of linguistic expressions. Our experiments and results show that the smart contract with the higher degrees of truth can be very complex technically but more accurate at the same time. By using fuzzy logic inside a smart contract, it becomes easier to solve the problem of contractual ambiguities as well as expedite the process of claiming compensation when implemented in a blockchain-based smart contract.

The challenge of implementing and executing a legal contract in a machine has been gaining significant interest recently with the advent of blockchain, smart contracts, LegalTech and IoT technologies. Popular software engineering methods, including agile ones, are unsuitable for such outcome-critical software. Instead, formal specifications are crucial for implementing smart contracts to ensure they capture the intentions of stakeholders, also that their execution is compliant with the terms and conditions of the original natural-language legal contract. This thesis concerns supporting the semi-automatic generation of formal specifications of legal contracts written in Natural Language (NL). The main contribution is a framework, named Contratto, where the transformation process from NL to a formal specification is subdivided into 5 steps: (1) identification of ambiguous terms in the contract and manual disambiguation; (2) structural and semantic annotation of the legal contract; (3) discovery of relationships among the concepts identified in step (2); (4) formalization of the terms used in the NL text into a domain model; (5) generation of formal expressions that describe what should be implemented by programmers in a smart contract. A systematic literature review on the main topic of the thesis was performed to support the definition of the framework. Requirements were derived from standard business contracts for a preliminary implementation of tools that support the transformation process, particularly concerning step (2). A prototype environment was proposed to semi-automate the transformation process although significant manual intervention is required. The preliminary evaluation confirms that the annotation tool can perform the annotation as well as human annotators, albeit novice ones.