图1 智能合约的MDE要领流程
基于这个案例，本文针对智能合约存在的可信与安详问题，将形式化要领应用于智能合约的生命周期验证，从形式化描写和形式化验证要领方面举办了具体的叙述。一个好的模子检测东西有助于查抄和验证智能合约的各项属性。通过实例可以看出，智能合约可以在合约的差异节段得到差异的状态，当智能合约验证时，SPIN可以随机发生若干种差异的功效,形式化要领可以在智能合约的成立、验证和代码生成中获得重要应用，是智能合约可信和安详性的成长偏向。
我们可以简朴成立SSC的Promela模子如下：
图 4 模子模仿功效（超时退款）
2. 智能合约的验证案例
智能购物合约的描写如下：当用户下订单时，他需要将购物所需的资金提交给智能购物合约，智能购物合约临时持有资金。同时SSC启动两个子历程，用户历程和商店历程。用户历程：假如商家在七天内没有交货，用户将打消生意业务，SSC会将资金退还给用户，用户历程按时、周期地检测交货状态；商店历程：商家收到订单后，系统判定订单是否竣事，假如订单没有超时，则商店发货。SSC需要确保资金的安详性和生意业务进程中各个状态的可达性。
图5 模子模仿功效（生意业务完成）
智能合约形式化验证文章作者：北航云南数字经济研究中心 我要纠错
MDE可以支持智能合约的整个生命周期，从建模、验证、代码生成到一致性测试，应用于智能合约的形式化要领流程如图 1所示。
合约2: 售后处事合约:
合约1: 货品订购与分派：
北京航空航天大学漫衍式尝试室 北京航空航天大学云南创新研究院 白晓敏，周楚涵
根基合约包罗商品订货、分销和售后处事，合约可以组合和定制。
声明：本文由入驻金色财经的作者撰写，概念仅代表作者本人，毫不代表金色财经附和其概念或证实其描写。
1. MDE要领工程框架
图 2 MDA形式化要领应用框架
我们利用Promela建模语言和检测东西SPIN来成立和验证一个互联网智能购物合约SSC（Smart Shopping Contract）的模子。
然后我们可以利用模子检测东西SPIN检测SSC模子，模子的模仿功效如4所示。从图4的模子仿真功效可以看出，，一旦超时（day= 8），SSC将钱退还给用户。
在模子驱动框架下，由于体系布局模子包括的系统特征和信息较多，一般不直接对体系布局模子举办验证和阐明，而主要回收模子转换的方法，即将体系布局模子（或子集）转换到另一个形式模子，可能直接转换到模子检测东西或定理证明器，目标是为了重用这些已有的验证和阐明本领。我们提出智能合约的模子检测工程化形式化要领框架如图 2所示。一个合约的生成包罗：首先，用户提出需求，按照用户需求拟定合约文本。然后对合约文本举办形式化描写，并选择符合的建模语言和建模东西对形式化规格说明文档举办建模和性质验证。个中，模子验证包罗理论证明和模子检测，在模子检测中，我们凡是利用模子转换来验证更多的性质。最后是一致性测试。为了证明合约代码与合约文本在性质和执行力是保持一致的，因此，需要对合约文本和合约代码举办一致性测试。这就是将形式化要领应用于智能合约完整生命周期的框架。
SSC应在用户订单之后触发，而且它具有两个参加者，即用户和商店。
本文将先容基于模子检测形式化要领应用于智能合约帮助生成和验证的一个案例，便于各人相识相关的技能蹊径。作为形式化要领的工程实践，模子驱动工程（MDE）旨在提高措施类型中的抽象级别，从而提高措施类型中的抽象级别，通过利用可执行模子转换来增加措施开拓中的自动化，较高级此外模子被转换为较初级此外模子，直到该模子可以利用代码生成或模子表明来执行。
如图 5功效所示，当商店在第二天送货时，SSC将钱转给商店。由于SSC是有限状态模子，通过对SSC的建模和验证，SPIN可以随机生成合约的所有状态，尝试功效与合约的预期功效一致。
郑重声明：本文版权归原作者所有，转载文章仅为传播更多信息之目的，如作者信息标记有误，请第一时间联系我们修改或删除，多谢。
