Integrating Business Process Context into Solidity-to-CPN Formal Verification

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.