2008年中本聪(Satoshi Nakamoto)首次提出了区块链的概念,在过去的十几年中,区块链技术凭借其去中心化、公开透明以及不可篡改等特性而被广泛应用,其中最具代表性的是以太坊(Ethereum)。以太坊是一个开源的区块链系统,提供了丰富的接口,任何人都可以在以太坊上开发智能合约程序,以太坊中大多数智能合约都是用Solidity语言编写的。以太坊为智能合约提供了天然的执行平台,智能合约能够为以太坊自动处理复杂的业务逻辑。随着智能合约被广泛使用,合约漏洞事件却层出不穷,智能合约的安全性引起了人们的关注。在智能合约部署到区块链系统之前,对其进行安全审计是至关重要的。由于智能合约与用户的财产安全直接相关,传统的测试手段并不能满足审计的需求。形式化方法采用数学推理的方式来验证系统的安全性,本文将形式化方法中的模型检测应用于智能合约的建模与验证,基本思想是首先描述待验证系统的模型,然后描述待验证系统的性质,最后验证模型是否满足性质。为实现对智能合约程序需求、结构、行为以及参数约束等各方面的描述,需要一种定义良好、易于表达且普遍适用的标准建模语言。本文提出了一种基于时序逻辑程序设计语言(Modeling,Simulation and Verification Language,MSVL)的智能合约建模与验证方法。首先,使用MSVL对Solidity语言编写的智能合约程序进行建模,为了减少建模过程中大量的人工操作,开发了基于JavaCC(Java Compiler Compiler)的转换器SOL2M,可以将Solidity程序自动转换为MSVL程序。给出了SOL2M转换器的整体架构,并分别从预处理、词法分析、语法分析以及程序转换四个模块对其具体实现流程进行了详细介绍。之后,为了给智能合约建模程序的运行提供基础的结构与数据,使用MSVL程序对区块链底层进行了抽象建模。然后,为了能够对智能合约程序进行递进式验证,使用命题投影时序逻辑(Propositional Projection Temporal Logic,PPTL)公式分别从功能一致性、逻辑正确性以及合约完备性三个方面对合约的性质进行描述。最后,将描述模型的MSVL程序和描述性质的PPTL公式统一到MSVL模型检测器(Unified Model Checker for MSVL,UMC4M)中进行验证,根据验证结果来完善智能合约程序进而保证合约的完备性。基于上述方法及工具,通过具体的投票智能合约实例表明该方法的有效性以及可行性。