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.
维普
万方数据