带时间约束的智能合约验证
赵颖琪, 朱雪阳, 李广元, 高雅, 包玉龙
中国科学院软件研究所计算机科学国家重点实验室
中国科学院大学
在现实生活中有一类智能合约与时间紧密相关,而合约是否满足这类时间性质将直接影响应用的正确性。为了避免合约部署后出现严重的问题,将以太坊上的智能合约为研究对象定义智能合约的时间自动机语义,再将智能合约转换为时间自动机模型,接着用模型检测工具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
领取专属 10元无门槛券
私享最新 技术干货