典型文献
智能合约的时间约束模式及其形式化验证
文献摘要：
智能合约是一套以数字形式定义的承诺.通过智能合约,可以大大减少协议制定的中间环节,提高协议制定的效率.区块链技术为智能合约的执行提供了可信平台.随着区块链应用的拓广与深入,智能合约的作用必然越来越突出,智能合约的可靠性问题也将更加突显.以提高智能合约可靠性为目的的研究日益得到重视,但尚未有人对智能合约的时间性质可能引起的可靠性问题进行过系统的研究.通过分析典型智能合约,对智能合约时间约束的不同表现形式进行梳理,提炼出相应的时间约束模式并对其进行形式化;定义Solidity智能合约到时间自动机的转换规则,并实现其到实时模型检测工具UPPAAL入口模型的自动转换;再利用UPPAAL验证合约的时间相关性质.最后对两个实际合约进行实例研究,结果表明了所提炼模式的普遍性以及所提出形式化验证方案的可行性和有效性.
文献关键词：
智能合约;时间约束模式;模型检测;Solidity;形式化方法
中图分类号：
作者姓名：
赵颖琪;朱雪阳;李广元;包玉龙
作者机构：
计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 100049
文献出处：
引用格式：
[1]赵颖琪;朱雪阳;李广元;包玉龙-.智能合约的时间约束模式及其形式化验证)[J].软件学报,2022(08):2875-2895
A类：
时间约束模式
B类：
智能合约,形式化验证,字形,大大减少,中间环节,区块链应用,拓广,高智能,时间性,Solidity,时间自动机,转换规则,模型检测,检测工具,UPPAAL,口模,自动转换,时间相关性,实例研究,形式化方法
AB值：
0.272017
相似文献
机标中图分类号，由域田数据科技根据网络公开资料自动分析生成，仅供学习研究参考。
