文献类型：期刊文章

作　　者：胡凯[1] 白晓敏[1] 高灵超[2] 董爱强[2]

机构地区：[1]北京航空航天大学计算机学院,北京100191 [2]北京中电普华信息技术有限公司,北京100192

出　　处：《信息安全研究》

基　　金：国家自然科学基金项目(91538202)

年　　份：2016

卷　　号：2

期　　号：12

起止页码：1080-1089

语　　种：中文

收录情况：NSSD、RCCSE、ZGKJHX、普通刊

摘　　要：智能合约是一种代码合约和算法合同,将成为未来数字社会的基础技术,它利用协议和用户接口,完成合约过程的所有步骤.总结了智能合约主要技术特点和现存的可信、安全等问题,提出将形式化方法应用于智能合约的建模、模型检测和模型验证过程,以支持规模化智能合约的生成.研究提出了一个应用于智能合约生命周期的形式化验证框架和验证方法,针对一个智能购物场景,采用Promela建模语言对智能购物合约进行建模,用SPIN进行了模型检测,验证了形式化方法对智能合约的作用.

关 键 词：智能合约  形式化方法 建模  验证  SPIN模型检测工具  

分 类 号：TP301]