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