论文部分内容阅读
智能合约是运行在区块链上的计算机协议,被广泛应用在各个领域中,但是其安全问题层出不穷,因此在智能合约部署到区块链上之前,需要对其进行安全审计.然而,传统的测试方法无法保证智能合约所需的高可靠性和正确性.说明了如何使用建模、仿真与验证语言(MSVL)和命题投影时序逻辑(PPTL)对智能合约进行建模和验证:首先介绍了MSVL与PPTL的理论基础;之后,通过分析和对比Solidity与MSVL语言的特性,开发了能够将Solidity程序转换为MSVL程序的SOL2M转换器,并详细介绍了SOL2M转换器的设计思路