一种基于UPPAAL的智能合约属性形式化验证方法  

The Formal Verification Method for Smart Contract Properties Based on UPPAAL

作　　者：张取发 王昌晶[1,2] 左正康 卢家兴[1] 廖云燕[1] 王渊[3] ZHANG Qufa;WANG Changjing;ZUO Zhengkang;LU Jiaxing;LIAO Yunyan;WANG Yuan(School of Computer and Information Engineering,Jiangxi Normal University,Nanchang Jiangxi 330022,China;Management Science and Engineering Research Center,Jiangxi Normal University,Nanchang Jiangxi 330022,China;School of Software,Jiangxi Normal University,Nanchang Jiangxi 330027,China)

机构地区：[1]江西师范大学计算机信息工程学院,江西南昌330022 [2]江西师范大学管理科学与工程研究中心,江西南昌330022 [3]江西师范大学软件学院,江西南昌330027

出　　处：《江西师范大学学报（自然科学版）》2023年第1期45-51,共7页Journal of Jiangxi Normal University(Natural Science Edition)

基　　金：江西省教育厅科技重点课题(GJJ220302,GJJ210307,GJJ2200303,GJJ2200304)资助项目.

摘　　要：针对智能合约的属性验证问题,该文提出了一种基于UPPAAL的智能合约属性形式化验证方法.首先定义了Solidity基本语句的操作语义及其到时间自动机的转换,将智能合约转换成时间自动机网络模型;然后定义并描述智能合约常见的安全性和活性,再使用模型检测工具UPPAAL验证智能合约的属性;最后对购物合约进行了建模与验证,验证了该方法的有效性.Aiming at the problem of smart contract property verification,the formal verification method of smart contract properties based on UPPAAL is proposed in this paper.The operational semantics of Solidity basic statements and its transformation to time automata are defined,and smart contracts are transformed into time automata network models.The properties of smart contracts include safety and activity.The common security and activity of smart contracts are defined and described.The model checking tool UPPAAL is used to verify the properties of smart contracts.The shopping contract is modeled and verified,which proves the effectiveness of the proposed method.

关 键 词：智能合约 UPPAAL 时间自动机 安全性 活性 

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