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...
Saved in:
| Main Authors: | , , , , , |
|---|---|
| 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!
|
| _version_ | 1846141157275336704 |
|---|---|
| author | Rui Xie Xuejiao Zhong Xin Chen Shaohui Xu Haiyang Yu Xinyuan Guo |
| author_facet | Rui Xie Xuejiao Zhong Xin Chen Shaohui Xu Haiyang Yu Xinyuan Guo |
| author_sort | Rui Xie |
| collection | DOAJ |
| description | 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. |
| format | Article |
| id | doaj-art-dd747bd582774a80a3a51e51df9eec16 |
| institution | Kabale University |
| issn | 2158-3226 |
| language | English |
| publishDate | 2024-11-01 |
| publisher | AIP Publishing LLC |
| record_format | Article |
| series | AIP Advances |
| spelling | doaj-art-dd747bd582774a80a3a51e51df9eec162024-12-04T16:59:17ZengAIP Publishing LLCAIP Advances2158-32262024-11-011411115304115304-910.1063/5.0238456Automatic construction and verification algorithm for smart contracts based on formal verificationRui Xie0Xuejiao Zhong1Xin Chen2Shaohui Xu3Haiyang Yu4Xinyuan Guo5Huizhou Power Supply Bureau, Guangdong Power Grid Co., Ltd., Huizhou 516000, ChinaSouthern Power Grid Digital Enterprise Technology Co., Ltd., Huizhou 516000, ChinaHuizhou Power Supply Bureau, Guangdong Power Grid Co., Ltd., Huizhou 516000, ChinaHuizhou Power Supply Bureau, Guangdong Power Grid Co., Ltd., Huizhou 516000, ChinaSouthern Power Grid Digital Enterprise Technology Co., Ltd., Huizhou 516000, ChinaXi’an Jiaotong University, Xi’an 712000, ChinaAs 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.http://dx.doi.org/10.1063/5.0238456 |
| spellingShingle | Rui Xie Xuejiao Zhong Xin Chen Shaohui Xu Haiyang Yu Xinyuan Guo Automatic construction and verification algorithm for smart contracts based on formal verification AIP Advances |
| title | Automatic construction and verification algorithm for smart contracts based on formal verification |
| title_full | Automatic construction and verification algorithm for smart contracts based on formal verification |
| title_fullStr | Automatic construction and verification algorithm for smart contracts based on formal verification |
| title_full_unstemmed | Automatic construction and verification algorithm for smart contracts based on formal verification |
| title_short | Automatic construction and verification algorithm for smart contracts based on formal verification |
| title_sort | automatic construction and verification algorithm for smart contracts based on formal verification |
| url | http://dx.doi.org/10.1063/5.0238456 |
| work_keys_str_mv | AT ruixie automaticconstructionandverificationalgorithmforsmartcontractsbasedonformalverification AT xuejiaozhong automaticconstructionandverificationalgorithmforsmartcontractsbasedonformalverification AT xinchen automaticconstructionandverificationalgorithmforsmartcontractsbasedonformalverification AT shaohuixu automaticconstructionandverificationalgorithmforsmartcontractsbasedonformalverification AT haiyangyu automaticconstructionandverificationalgorithmforsmartcontractsbasedonformalverification AT xinyuanguo automaticconstructionandverificationalgorithmforsmartcontractsbasedonformalverification |