文献类型：期刊文献

中文题名：基于CPN的供应链合约的形式化验证

英文题名：Formal Verification of Supply Chain Contract Based on Coloured Petri Nets

作者：郑红[1];钱诗慧[1];刘泽润[1];杜渂[2]

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

年份：2023

卷号：50

期号：S01

起止页码：707

中文期刊名：计算机科学

外文期刊名：Computer Science

收录：CSTPCD;;北大核心:【北大核心2020】；CSCD:【CSCD_E2023_2024】；

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

语种：中文

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

外文关键词：Smart contract;Formal methods;Model checking;CPN;Supply chain

摘要：智能合约的安全性对于区块链在供应链领域的应用尤为重要。目前,大多数对智能合约的形式化验证工作集中于漏洞检测,对于如何在部署上链前生成安全的智能合约的关注仍然比较少,如何有效规范地将特定领域的属性安全地映射为智能合约代码存在难点。因此,提出在编写合约前基于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.