摘要
为提升拍卖合约时间安全性验证效率及验证公平性,提出基于角色的拍卖合约抽象建模及其验证方法。首先,对合约源代码进行基于账户角色的抽象建模,转换为时间自动机网络模型,并对时间安全性进行形式化描述,用UPPAAL工具验证。其次,提取合约源代码机制,建立智能合约机制模型,同样转换为时间自动机网络模型,并对4种公平性进行形式化描述,再用UPPAAL验证。最后,通过2个经典案例证明了所提方法的可行性和有效性。
To enhance the efficiency of time security verification and fairness verification of auction contracts,an abstract 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 descriptions 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.
作者
王昌晶
欧阳俊媛
张取发
左正康
程着
卢家兴
WANG Changjing;OUYANG Junyuan;ZHANG Qufa;ZUO Zhengkang;CHENG Zhuo;LU Jiaxing(School of Computer and Information Engineering,Jiangxi Normal University,Nanchang 330022,China;School of Software,East China University of Technology,Nanchang 330013,China;National-level International Science and Technology Cooperation Base of Networked Supporting Software,Jiangxi Normal University,Nanchang 330022,China)
出处
《通信学报》
EI
CSCD
北大核心
2024年第10期225-242,共18页
Journal on Communications
基金
国家自然科学基金资助项目(No.62462037,No.62462036)
江西省主要学科学术与技术带头人培养基金资助项目(No.20232BCJ22013)
江西省自然科学基金资助项目(No.20242BAB26017)
江西省教育厅科技基金资助项目(No.GJJ2200303,No.GJJ210340)。
