TY - GEN
T1 - Integrating Business Process Context into Solidity-to-CPN Formal Verification
AU - Garfatta, Ikram
AU - Klai, Kaïs
AU - Gaaloul, Walid
N1 - Publisher Copyright:
© 2024 IEEE.
PY - 2024/1/1
Y1 - 2024/1/1
N2 - Smart contracts, which are self-executing agreements, have a huge range of possible uses from finance to supply chain management. To avoid costly errors and vulnerabilities, it is crucial to guarantee the accuracy and reliability of these contracts. This paper explores the convergence of Blockchain technology, particularly Ethereum's smart contracts, and Business Process Modeling (BPM), capitalizing on the synergies between these domains. We propose that viewing smart contracts as akin to business processes can significantly enhance the verification of Blockchain-based applications, addressing critical challenges in smart contract correctness and security. In this work we employ a formal verification approach based on Coloured Petri Nets and Linear Temporal Logic to detect potential vulnerabilities in Solidity smart contracts while considering their behavioral context as a business process model.
AB - Smart contracts, which are self-executing agreements, have a huge range of possible uses from finance to supply chain management. To avoid costly errors and vulnerabilities, it is crucial to guarantee the accuracy and reliability of these contracts. This paper explores the convergence of Blockchain technology, particularly Ethereum's smart contracts, and Business Process Modeling (BPM), capitalizing on the synergies between these domains. We propose that viewing smart contracts as akin to business processes can significantly enhance the verification of Blockchain-based applications, addressing critical challenges in smart contract correctness and security. In this work we employ a formal verification approach based on Coloured Petri Nets and Linear Temporal Logic to detect potential vulnerabilities in Solidity smart contracts while considering their behavioral context as a business process model.
KW - Business Process Modeling
KW - Coloured Petri Nets
KW - Formal Verification
KW - Linear Temporal Logic
KW - Solidity
UR - https://www.scopus.com/pages/publications/85218964120
U2 - 10.1109/WETICE64632.2024.00021
DO - 10.1109/WETICE64632.2024.00021
M3 - Conference contribution
AN - SCOPUS:85218964120
T3 - Proceedings of the Workshop on Enabling Technologies: Infrastructure for Collaborative Enterprises, WETICE
SP - 68
EP - 73
BT - Proceedings - 2024 32nd International Conference on Enabling Technologies
PB - IEEE Computer Society
T2 - 32nd International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises, WETICE 2024
Y2 - 26 June 2024 through 28 June 2024
ER -