软件学报

作者：赵颖琪，朱雪阳，李广元，包玉龙

单位：赵颖琪，计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 10004911,朱雪阳，计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 10004902,李广元，计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 10004903,包玉龙，计算机科学国家重点实验室(中国科学院 软件研究所), 北京 10019004

关键词：智能合约;时间约束模式;模型检测;Solidity;形式化方法

基金：国家自然科学基金(62072443)

智能合约是一套以数字形式定义的承诺.通过智能合约,可以大大减少协议制定的中间环节,提高协议制定的效率.区块链技术为智能合约的执行提供了可信平台.随着区块链应用的拓广与深入,智能合约的作用必然越来越突出,智能合约的可靠性问题也将更加突显.以提高智能合约可靠性为目的的研究日益得到重视,但尚未有人对智能合约的时间性质可能引起的可靠性问题进行过系统的研究.通过分析典型智能合约,对智能合约时间约束的不同表现形式进行梳理,提炼出相应的时间约束模式并对其进行形式化;定义Solidity智能合约到时间自动机的转换规则,并实现其到实时模型检测工具UPPAAL入口模型的自动转换;再利用UPPAAL验证合约的时间相关性质.最后对两个实际合约进行实例研究,结果表明了所提炼模式的普遍性以及所提出形式化验证方案的可行性和有效性.

来源：2022年第8期

《软件学报》期刊编辑部

查看软件学报杂志2022年第8期