JHCIE194-2021区块链智能合约形式化设计与验证方法.pdf

中国电子学会标准

JH/CIE194—2021

区块链智能合约形式化设计与验证方法

Formaldesignandverificationmethodofblockchainsmartcontract

（征求意见稿）

（本稿完成时间：2022年1月26日）

在提交反馈意见时，请将您知道的相关专利连同支持性文件一并附上。

XXXX-XX-XX发布XXXX-XX-XX实施

中国电子学会发布

JH/CIE194-2021

目次

前言3

1范围1

2规范性引用文件1

3术语和定义1

4符号3

5概述4

6智能合约需求描述5

7智能合约形式化建模9

8模型转换10

9智能合约形式化模型验证11

10自动代码生成与一致性测试15

11智能合约代码20

附录A21

附录B24

附录C27

附录D30

参考文献32

JH/CIE194-2021

区块链智能合约形式化设计与验证方法

1范围

本文件规定了使用形式化设计区块链智能合约要求，描述了对应的智能合约验证方法。

本文件适用于采用形式化方法设计、开发可信通用区块链智能合约的应用场景。

2规范性引用文件

下列文件对于本文件的应用是必不可少的。凡是注日期的引用文件，仅注日期的版本适用于本文件。

凡是未注日期的引用文件，其必威体育精装版版本（包括所有的修改单）适用于本文件。

GB/T22032-2021系统与软件工程系统生存周期过程

GB/T11457-2006信息技术软件工程术语

中国电子学会标准T/CIE095—2020区块链智能合约形式化表达

3术语和定义

下列术语和定义适用于本文件。

3.1

需求分析demandanalysis

创建一个新的或改变一个现存的系统或产品时，确定新系统的目的、范围、定义和功能时所要做的

所有工作。

3.2

区块链智能合约blockchainsmartcontract

部署在区块链上并可在满足预定合约条款和履行条件时自动执行的计算机代码。

3.3

形式化设计方法formaldesignmethods

包括智能合约的形式化建模、形式模型的一致性转换、形式模型的验证、可执行代码的自动生成以

及一致性测试，使用形式化方法涵盖了智能合约全生命周期的设计与验证过程，以保证智能合约需求设

计与描述的正确性、智能合约代码的安全性、智能合约功能属性和非功能属性的可靠性，并通过代码的

自动生成提高开发效率，通过设计迭代提高可维护性。

3.4

领域特定语言domain-specificlanguage

1

JH/CIE194-2021

某个应用程序领域的计算机语言，面向某些智能合约应用场景的计算机描述语言。

3.5

智能合约语言smartcontractlanguage

一种为实现智能合约而创建的编程语言，包含规范智能合约撰写的语法规则和语义，具有图灵完备

性。

3.6

形式化方法formalmethods

基