Time Constraint Patterns of Smart Contracts and Their Formal Verification

Abstract

Smart contract consists of a set of commitments defined in digital form. Smart contracts can greatly reduce the intermediate links in agreement formulation and improve the efficiency of agreement formulation. Blockchain technology provides a trusted platform for the execution of smart contracts. As the application of blockchain technology expands and deepens, the role of smart contracts will become more and more important, and the potential reliability problems, however, may cause huge lose to participants. The reliability of smart contracts has received more and more attention, but there is no systematic research on problems caused by the time properties of smart contracts. This study analyzes typical smart contracts, sorts out the different manifestations of time constraints, summarizes several time constraint patterns of smart contracts and formalizes them; defines transform rules from Solidity smart contracts to the timed automata. The translation from smart contracts to the model of model checker UPPAAL is then implemented and UPPAAL is used to verify the time properties of smart contracts. Case study is carried out on two practical smart contracts. The results show that the patterns extracted are general and the formal verification solution proposed is feasible and efficient.