带时间约束的智能合约验证

在现实生活中有一类智能合约与时间紧密相关，而合约是否满足这类时间性质将直接影响应用的正确性。为了避免合约部署后出现严重的问题，将以太坊上的智能合约为研究对象定义智能合约的时间自动机语义，再将智能合约转换为时间自动机模型，接着用模型检测工具UPPAAL检测智能合约是否满足以时序逻辑公式表示的实时性质。最后对竞拍合约以及飞机保险购买合约进行了实例研究，其结果可以展示合约的实时性质是否得以满足。若不满足则可以根据反例定位合约出现的问题点，显示了该工作的有效性。

Verification of Smart Contracts with Time Constraints

In real life, a type of smart contract is closely related to time constraint, and whether the contract meets its time property will directly affect the correctness of its applications. In order to avoid serious problems after its deployment, this paper focuses on smart contracts of Ethereum, gives a timed automata semantics for smart contracts, after the smart contract is converted into a time automata model, and uses model checking tool UPPAAL to check whether the smart contract meets timed properties expressed by temporal logic formulas. Finally, we study two cases, an auction contract and a flight insurance contract. Experimental results indicate whether the real-time property is satisfied. If not, counter examples can be used to locate the problem points in the smart contract, showing the effectiveness of the work.