收稿日期:2022-11-21基金项目:江西省教育厅科技重点课题(GJJ220302，GJJ210307，GJJ2200303，GJJ2200304)资助项目．通信作者:王昌晶(1977—)，男，江西丰城人，教授，博士，博士生导师，主要从事可信软件、智能化软件与智能化教育的研究．E-mail:wcj@jxnu．edu．cn卢家兴(1976—)，男，江西九江人，副教授，主要从事软件形式化方法、模型检测方面的研究．E-mail:003484@jxnu．edu．cn张取发，王昌晶，左正康，等．一种基于UPPAAL的智能合约属性形式化验证方法［J］．江西师范大学学报(自然科学版)，2023，47(1):45-51．ZHANGQufa，WANGChangjing，ZUOZhengkang，etal．TheformalverificationmethodforsmartcontractpropertiesbasedonUPPAAL［J］．JournalofJiangxiNormalUniversity(NaturalScience)，2023，47(1):45-51．文章编号:1000-5862(2023)01-0045-07一种基于UPPAAL的智能合约属性形式化验证方法张取发1，王昌晶1，2*，左正康1，卢家兴1*，廖云燕1，王渊3(1．江西师范大学计算机信息工程学院，江西南昌330022;2．江西师范大学管理科学与工程研究中心，江西南昌330022;3．江西师范大学软件学院，江西南昌330027)摘要:针对智能合约的属性验证问题，该文提出了一种基于UPPAAL的智能合约属性形式化验证方法．首先定义了Solidity基本语句的操作语义及其到时间自动机的转换，将智能合约转换成时间自动机网络模型;然后定义并描述智能合约常见的安全性和活性，再使用模型检测工具UPPAAL验证智能合约的属性;最后对购物合约进行了建模与验证，验证了该方法的有效性．关键词:智能合约;UPPAAL;时间自动机;安全性;活性中图分类号:TP311文献标志码:ADOI:10．16357/j．cnki．issn1000-5862．2023．01．060引言区块链是一种安全共享的去中心化的数据账本，智能合约是部署在区块链网络上的计算机程序［1］，当满足必要条件时，它就会自动执行．早在1994年，N．Szabo［2］就提出了智能合约的概念，他指出“一个智能合约是一套数字形式定义的承诺，包括合约的参与方可以在上面执行这些承诺的协议”．随着具有去中心化和公开透明等特性的区块链技术出现，智能合约的信任问题得到了有效解决．目前，以太坊［3］已成为主流的智能合约开发和运行的平台．智能合约包含了区块链的众多特性，使得区块链与智能合约技术在许多领域都得到了广泛的应用．尽管智能合约发展迅速，但智能合约的执行代码不能保证绝对安全，且智能合约运行时往往会伴随着大量数字资产的存储和转...
