北京航空航天大学分布式实验室 北京航空航天大学云南创新研究院 白晓敏，周楚涵
本文将介绍基于模型检测形式化方法应用于智能合约辅助生成和验证的一个案例，便于大家了解相关的技术路线。作为形式化方法的工程实践，模型驱动工程（MDE）旨在提高程序规范中的抽象级别，从而提高程序规范中的抽象级别，通过使用可执行模型转换来增加程序开发中的自动化，较高级别的模型被转换为较低级别的模型，直到该模型可以使用代码生成或模型解释来执行。
1. MDE方法工程框架
MDE可以支持智能合约的整个生命周期，从建模、验证、代码生成到一致性测试，应用于智能合约的形式化方法流程如图 1所示。
图1 智能合约的MDE方法流程
在模型驱动框架下，由于体系结构模型包含的系统特征和信息较多，一般不直接对体系结构模型进行验证和分析，而主要采用模型转换的方式，即将体系结构模型（或子集）转换到另一个形式模型，或者直接转换到模型检测工具或定理证明器，目的是为了重用这些已有的验证和分析能力。我们提出智能合约的模型检测工程化形式化方法框架如图 2所示。一个合约的生成包括：首先，用户提出需求，根据用户需求制定合约文本。然后对合约文本进行形式化描述，并选择合适的建模语言和建模工具对形式化规格说明文档进行建模和性质验证。其中，模型验证包括理论证明和模型检测，在模型检测中，我们通常使用模型转换来验证更多的性质。最后是一致性测试。为了证明合约代码与合约文本在性质和执行力是保持一致的，因此，需要对合约文本和合约代码进行一致性测试。这就是将形式化方法应用于智能合约完整生命周期的框架。
图 2 MDA形式化方法应用框架
2. 智能合约的验证案例
我们使用Promela建模语言和检测工具SPIN来建立和验证一个互联网智能购物合约SSC（Smart Shopping Contract）的模型。
SPIN是一个通用的形式化验证工具，以严格的和大多数自动化的方式验证分布式软件模型的正确性。是一种著名的分析验证并发系统逻辑一致性的工具，以其简洁明了和自动化程度高而备受注目。SPIN已成功应用在安全协议验证、控制系统验证、软件验证及最优化规划等领域。作为一种形式化自动验证工具，SPIN可以提供：1）系统建模语言Promela（Process Meta Language），用于直观、明确地描述系统Promela模型规约，而不考虑具体实现细节；2）功能强大而简明的描述系统应满足性质（属性要求）的逻辑表示法；3）提供一套验证系统建模逻辑一致性及系统是否满足所要验证性质的方法。除模型检测之外，SPIN还可以作为模拟器操作，遵循系统的一个可能的执行路径并且向用户呈现所产生的执行轨迹。
基本合约包括商品订货、分销和售后服务，合约可以组合和定制。
合约1: 货物订购与分配：
合约2: 售后服务合约:
SSC应在用户订单之后触发，并且它具有两个参与者，即用户和商店。
智能购物合约的描述如下：当用户下订单时，他需要将购物所需的资金提交给智能购物合约，智能购物合约暂时持有资金。同时SSC启动两个子进程，用户进程和商店进程。用户进程：如果商家在七天内没有交货，用户将取消交易，SSC会将资金退还给用户，用户进程定时、周期地检测交货状态；商店进程：商家收到订单后，系统判断订单是否结束，如果订单没有超时，则商店发货。SSC需要确保资金的安全性和交易过程中各个状态的可达性。
我们可以简单建立SSC的Promela模型如下：
然后我们可以使用模型检测工具SPIN检测SSC模型，模型的模拟结果如4所示。从图4的模型仿真结果可以看出，一旦超时（day= 8），SSC将钱退还给用户。
图 4 模型模拟结果（超时退款）
如图 5结果所示，当商店在第二天送货时，SSC将钱转给商店。由于SSC是有限状态模型，通过对SSC的建模和验证，SPIN可以随机生成合约的所有状态，实验结果与合约的预期结果一致。
图5 模型模拟结果（交易完成）
基于这个案例，本文针对智能合约存在的可信与安全问题，将形式化方法应用于智能合约的生命周期验证，从形式化描述和形式化验证方法方面进行了详细的阐述。一个好的模型检测工具有助于检查和验证智能合约的各项属性。通过实例可以看出，智能合约可以在合约的不同节段获得不同的状态，当智能合约验证时，SPIN可以随机产生若干种不同的结果,形式化方法可以在智能合约的建立、验证和代码生成中得到重要应用，是智能合约可信和安全性的发展方向。
智能合约形式化验证文章作者：北航云南数字经济研究中心 我要纠错
声明：本文由入驻金色财经的作者撰写，观点仅代表作者本人，绝不代表金色财经赞同其观点或证实其描述。