软件学报

作者：王小兵，杨潇钰，舒新峰，赵亮

单位：王小兵，西安电子科技大学 计算机科学与技术学院, 陕西 西安 71007111,杨潇钰，西安电子科技大学 计算机科学与技术学院, 陕西 西安 71007102,舒新峰，西安邮电大学 计算机学院, 陕西 西安 71012103,赵亮，西安电子科技大学 计算机科学与技术学院, 陕西 西安 71007104

关键词：区块链;智能合约;形式化方法;MSVL

基金：国家自然科学基金（61672403，61972301）；陕西省重点研发计划（2020GY-043，2020GY-210）

智能合约是运行在区块链上的计算机协议，被广泛应用在各个领域中，但是其安全问题层出不穷，因此在智能合约部署到区块链上之前，需要对其进行安全审计.然而，传统的测试方法无法保证智能合约所需的高可靠性和正确性.说明了如何使用建模、仿真与验证语言（MSVL）和命题投影时序逻辑（PPTL）对智能合约进行建模和验证：首先介绍了MSVL与PPTL的理论基础；之后，通过分析和对比Solidity与MSVL语言的特性，开发了能够将Solidity程序转换为MSVL程序的SOL2M转换器，并详细介绍了SOL2M转换器的设计思路；最终，通过投票智能合约和银行转账智能合约两个实例，给出了SOL2M转换器的执行结果.使用PPTL从功能一致性、逻辑正确性以及合约完备性这3个方面描述了合约的性质，给出了使用统一模型检测器（UMC4M）对合约进行验证的过程.

来源：2021年第6期

《软件学报》期刊编辑部

查看软件学报杂志2021年第6期