首页|基于角色的区块链拍卖合约抽象建模及其时间安全性与公平性验证

基于角色的区块链拍卖合约抽象建模及其时间安全性与公平性验证

扫码查看
原文链接
  • 万方数据
  • 维普
为提升拍卖合约时间安全性验证效率及验证公平性,提出基于角色的拍卖合约抽象建模及其验证方法.首先,对合约源代码进行基于账户角色的抽象建模,转换为时间自动机网络模型,并对时间安全性进行形式化描述,用UPPAAL工具验证.其次,提取合约源代码机制,建立智能合约机制模型,同样转换为时间自动机网络模型,并对4种公平性进行形式化描述,再用UPPAAL验证.最后,通过2个经典案例证明了所提方法的可行性和有效性.
Role-based abstract modeling of blockchain auction contracts and verification of temporal security and fairness
To enhance the efficiency of time security verification and fairness verification of auction contracts,an ab-stract modeling and verification method for role-based auction contracts was proposed.Firstly,the source code of the contract was abstractly modeled based on account roles and converted into a timed automaton network model.Formal de-scriptions of time security were provided and verified using the UPPAAL tool.Secondly,the mechanisms in the source code of the contract were extracted to establish a smart contract mechanism model,which was also converted into a timed automaton network model.Formal descriptions of four types of fairness were provided and verified using UPPAAL.Finally,the feasibility and effectiveness of the proposed method were demonstrated through two classic cases.

auction contractstemporal securityfairnesstime automataUPPAAL

王昌晶、欧阳俊媛、张取发、左正康、程着、卢家兴

展开 >

江西师范大学计算机信息工程学院,江西 南昌 330022

东华理工大学软件学院,江西 南昌 330013

江西师范大学国家网络化支撑软件国际合作基地,江西 南昌 330022

拍卖合约 时间安全性 公平性 时间自动机 UPPAAL

国家自然科学基金资助项目国家自然科学基金资助项目江西省主要学科学术与技术带头人培养基金资助项目江西省自然科学基金资助项目江西省教育厅科技基金资助项目江西省教育厅科技基金资助项目Jiangxi Provincial Natural Science Foundation

624620376246203620232BCJ2201320242BAB26017GJJ2200303GJJ21034020232BAB202010

2024

10.11959/j.issn.1000-436x.2024074

通信学报
中国通信学会

通信学报

CSTPCD北大核心
影响因子：1.265
ISSN：1000-436X
年,卷(期)：2024.45(10)