Automatic construction and verification algorithm for smart contracts based on formal verification

As an emerging technology, blockchain demonstrates strong potential for applications in digital finance. As a core component of blockchain, the security and reliability of smart contracts is crucial. To ensure the high reliability of smart contracts, this study employs formal construction and verifi...

Full description

Saved in:
Bibliographic Details
Main Authors: Rui Xie, Xuejiao Zhong, Xin Chen, Shaohui Xu, Haiyang Yu, Xinyuan Guo
Format: Article
Language:English
Published: AIP Publishing LLC 2024-11-01
Series:AIP Advances
Online Access:http://dx.doi.org/10.1063/5.0238456
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:As an emerging technology, blockchain demonstrates strong potential for applications in digital finance. As a core component of blockchain, the security and reliability of smart contracts is crucial. To ensure the high reliability of smart contracts, this study employs formal construction and verification techniques based on game theory. Initially, the profit function is defined using distortion techniques, and a game model for supply chain participation is designed. However, the equilibrium solution of the two-party game does not represent the optimal solution for the supply chain system. Therefore, the study introduces third-party participation to optimize the equilibrium solution. Finally, a probability model detection method is used to verify the constructed smart contract model. The results show that the supply chain model, analyzed through formal methods, has attributes consistent with theoretical analysis. Consequently, the research on automatic construction and verification algorithms for smart contracts based on formal verification proves to be effective and feasible in practical applications.
ISSN:2158-3226