摘要
智能合约是一种以代码的方式执行合同条款的可计算交易协议,其应用场景与规模日益增长,承载着多达数十亿美元的各类资产。由于其代码缺陷可能会造成严重的经济损失,因此智能合约的可信开发成为技术关键。为此,提出了一种基于集合论语言Event-B的智能合约可信验证与自动生成方法。Event-B方法是一种基于精化的形式化方法,可用于规约、设计和验证软件系统。通过对智能合约的模型验证和可执行代码的自动生成技术,研发了自动转换工具EB2S,打通了形式化模型和智能合约编程语言的语义鸿沟和技术壁垒。最后,选取典型的在线支付智能合约场景,应用基于Event-B的智能合约模型自动生成合约代码,验证了EB2S转换工具的有效性。
Smart contract is a new computable transaction agreement that executes contract terms in code.Its application scenarios and scale are growing with each passing day,carrying up to billions of dollars of various assets.However,smart contracts may cause serious economics losses due to code defects.Therefore,the trusted development of smart contract is particularly critical.This paper proposes a method of trusted verification and automatic generation of smart contracts based on the set theory language Event-B,which is a formal method based on refinement and can be used for specification,design and verification of software systems.Through the model verification of smart contracts and the automatic generation technology of executable codes,an automatic conversion tool EB2S is developed,which bridges the semantic gap and technical barriers between formal models and smart contract programming languages.Finally,this paper selects a typical online payment smart contract scenario,and the smart contract design and verification method based on Event-B is applied to automatically generate the smart contract code,which verifies the effectiveness of the conversion tool.
作者
朱健
胡凯
王军
李洁
叶亚飞
时希言
ZHU Jian;HU Kai;WANG Jun;LI Jie;YE Yafei;SHI Xiyan(The 14th Research Institute of CETC,Nanjing 210039,China;School of Computer Science and Engineering,Beihang University,Beijing 100191,China;Yunnan Innovation Institute of Beihang University,Kunming 650233,China;School of Information,Beijing Wuzi University,Beijing 101149,China;School of Economics and Management,Beijing University of Chemical Technology,Beijing 100029,China)
出处
《计算机科学》
CSCD
北大核心
2023年第10期343-349,共7页
Computer Science
基金
北京市自然科学基金(M22040)
云南省重大科技专项(202103AN080001-001,202102AD080006)。
