基于Event-B的可靠智能合约自动生成方法

摘要：

智能合约是一种以代码的方式执行合同条款的可计算交易协议,其应用场景与规模日益增长,承载着多达数十亿美元的各类资产.由于其代码缺陷可能会造成严重的经济损失,因此智能合约的可信开发成为技术关键.为此,提出了一种基于集合论语言 Event-B的智能合约可信验证与自动生成方法.Event-B方法是一种基于精化的形式化方法,可用于规约、设计和验证软件系统.通过对智能合约的模型验证和可执行代码的自动生成技术,研发了自动转换工具 EB2 S,打通了形式化模型和智能合约编程语言的语义鸿沟和技术壁垒.最后,选取典型的在线支付智能合约场景,应用基于 Event-B的智能合约模型自动生成合约代码,验证了 EB2 S转换工具的有效性.

关键词：智能合约、Event-B方法、自动代码生成、Solidity合约、定理证明

所属期刊栏目：50

分类号：TP311.5(计算技术、计算机技术)

在线出版日期：2023-10-13（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：343-349