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

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

赵颖琪, 朱雪阳, 李广元, 高雅, 包玉龙

中国科学院软件研究所计算机科学国家重点实验室

中国科学院大学

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

引用本文

赵颖琪, 朱雪阳, 李广元, 高雅, 包玉龙. 带时间约束的智能合约验证[J]. 应用科学学报, 2021, 39(1): 1-16.

ZHAO Yingqi, ZHU Xueyang, LI Guangyuan, GAO Ya, BAO Yulong. Verification of Smart Contracts with Time Constraints[J]. Journal of Applied Sciences, 2021, 39(1): 1-16.

https://www.jas.shu.edu.cn/CN/10.3969/j.issn.0255-8297.2021.01.001