Abstract: Smart contract is a code contract and algorithm contract and will become the basis of future agreements in digital society. Smart Contract utilizes protocols and user interfaces to facilitate all steps of the contracting process. This paper summarized the main technical characteristics of smart contract and existing problems such as trustworthiness and security and proposed that formal method is applied to the smart contract modeling, model checking and model verification to support the large-scale generation of smart contract. In this paper, a formal verification framework and verification method for smart contract in the whole life circle of smart contract has been proposed. The paper presented a smart shopping scene, in which Promela language is used for modeling a SSC(smart shopping contract) and SPIN is used to simulate and model checking to verify the effect of formal method on smart contract.

Key words: smart contract, formal method, modeling, verification, SPIN

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

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