| 一种基于UPPAAL的智能合约属性形式化验证方法 |
| |
| 引用本文： | 张取发1,王昌晶1,2,左正康1,卢家兴1,廖云燕1,王 渊3. 一种基于UPPAAL的智能合约属性形式化验证方法[J]. 江西师范大学学报(自然科学版), 2023, 0(1): 45-51 |
| |
| 作者姓名： | 张取发1 王昌晶1 2 左正康1 卢家兴1 廖云燕1 王 渊3 |
| |
| 作者单位： | (1.江西师范大学计算机信息工程学院,江西 南昌 330022; 2.江西师范大学管理科学与工程研究中心,江西 南昌 330022; 3.江西师范大学软件学院,江西 南昌 330027) |
| |
| 基金项目： | 江西省教育厅科技重点课题(GJJ220302,GJJ210307,GJJ2200303,GJJ2200304)资助项目； |
| |
| 摘 要： | 针对智能合约的属性验证问题，该文提出了一种基于UPPAAL的智能合约属性形式化验证方法.首先定义了Solidity基本语句的操作语义及其到时间自动机的转换，将智能合约转换成时间自动机网络模型；然后定义并描述智能合约常见的安全性和活性，再使用模型检测工具UPPAAL验证智能合约的属性；最后对购物合约进行了建模与验证，验证了该方法的有效性.
|
| 关 键 词： | 智能合约 UPPAAL 时间自动机 安全性 活性 |
The Formal Verification Method for Smart Contract Properties Based on UPPAAL |
| |
| ZHANG Qufa1,WANG Changjing1,' target="_blank" rel="external">2,ZUO Zhengkang1,LU Jiaxing1,LIAO Yunyan1,WANG Yuan3. The Formal Verification Method for Smart Contract Properties Based on UPPAAL[J]. Journal of Jiangxi Normal University (Natural Sciences Edition), 2023, 0(1): 45-51 |
| |
| Authors: | ZHANG Qufa1,WANG Changjing1,' target=" _blank" rel=" external" >2,ZUO Zhengkang1,LU Jiaxing1,LIAO Yunyan1,WANG Yuan3 |
| |
| Affiliation: | (1.School of Computer and Information Engineering,Jiangxi Normal University,Nanchang Jiangxi 330022,China; 2.Management Science and Engineering Research Center,Jiangxi Normal University,Nanchang Jiangxi 330022,China; 3.School of Software,Jiangxi Normal University,Nanchang Jiangxi 330027,China) |
| |
| Abstract: | 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. |
| |
| Keywords: | smart contracts UPPAAL time automata safety activity |
|
| 点击此处可从《江西师范大学学报(自然科学版)》浏览原始摘要信息 |
|
点击此处可从《江西师范大学学报(自然科学版)》下载全文 |
|
