基于CPN的供应链合约的形式化验证  

Formal Verification of Supply Chain Contract Based on Coloured Petri Nets

作　　者：郑红[1] 钱诗慧 刘泽润 杜渂[2] ZHENG Hong;QIAN Shihui;LIU Zerun;DU Wen(School of Information Science and Engineering,East China University of Science and Technology,Shanghai 200237,China;First Research Institute of Telecommunications Technology,Shanghai 200032,China)

机构地区：[1]华东理工大学信息科学与工程学院,上海200237 [2]电信科学技术第一研究所,上海200032

出　　处：《计算机科学》2023年第S01期707-713,共7页Computer Science

基　　金：2019年度上海市信息化发展(大数据发展)专项资金项目(201901043)。

摘　　要：智能合约的安全性对于区块链在供应链领域的应用尤为重要。目前,大多数对智能合约的形式化验证工作集中于漏洞检测,对于如何在部署上链前生成安全的智能合约的关注仍然比较少,如何有效规范地将特定领域的属性安全地映射为智能合约代码存在难点。因此,提出在编写合约前基于CPN(Coloured Petri Net)对供应链业务逻辑进行形式化规范并构建双层仿真模型,以图形化界面描述交易状态变化,进行形式化验证和状态分析,从而在建模阶段就减少逻辑漏洞。最后,提供了一种从CPN建模语言到Solidity编写的合约的转换方法,以提高智能合约的安全性和可靠性。The security of smart contracts is particularly vital to the application of blockchain in the supply chain field.Currently,most of formal verification work on smart contracts focuses on vulnerability detection,and there is still relatively little attention to how to generate secure smart contracts before deploying them on chain,and there are difficulties in how to effectively and stan-dardly map the properties of specific fields to smart contracts.Therefore,this paper proposes formal specification of supply chain business logic based on coloured Petri Net(CPN)before writing contracts and constructing a two-layer simulation model with a graphical interface to describe transaction state changes for formal verification and state analysis,thus reducing logic vulnerabilities at the modeling stage.Finally,a conversion method from the CPN modeling language to contracts written in Solidity is provided to improve the security and reliability of smart contracts.

关 键 词：智能合约 形式化方法 模型检查 CPN 供应链 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]