Formal Verification of Smart Contracts Using Interface Automata

Emerging distributed ledger technologies - also known as blockchains - have recently become a hot research topic across a wide variety of industries due to their immutability, availability, security, and more importantly, their ability to execute multi-party agreements or business rules in the form of smart contracts. Smart contracts provide the means to automate and enforce contractual terms between the parties entering the agreement. It is important to guarantee the correctness of such contracts in order to avoid catastrophic events that may require human intervention. This paper presents a method that builds on the interface automata model of computation as a semantic domain to formalize smart contracts. The formal model of computation assigns a precise and unambiguous meaning to smart contracts. Loyalty points are discounts and bonuses provided by companies with the purpose of retaining their loyal customers. The proposed method is evaluated in the context of a loyalty points marketplace. The decentralized, distributed and immutable nature of blockchain provides an appealing platform for the implementation of a loyalty points marketplace, and the formal semantics based on interface automata ensure that violations of the agreement can be detected, and contractual clauses can be enforced by all parties involved in loyalty points transactions.