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.

While Blockchains can open intriguing opportunities of research in many application contexts, they come with the risk of bringing new unconventional problems. In fact, because of the monetary value they hold, Blockchains have been subject to many attacks. Smart contracts, which are at the core of second-generation Blockchains, have been proven to be the origin of such attacks due to the exploitable vulnerabilities their code may hold. It is therefore an essential requirement to prove the correctness of the smart contracts to be deployed on a Blockchain to ensure its protection. The existing approaches have been focusing on targeting generic vulnerabilities like reentrancy, without offering the possibility to check temporal-based contract-specific properties. In this paper, we aim to address smart contracts verification while supporting such properties. We propose and implement a transformation of Solidity smart contracts into Coloured Petri nets and investigate the capability of existing model checking tools to check specific temporal properties of the formally modeled contract.