Automatic Modeling and Verification of Smart Contracts Based on Colored Petri Nets

The tamper-proof feature of blockchain makes the correctness of smart contracts crucial before they are run on the chain. Using model checking methods to verify smart contracts helps ensure their correctness. Methods for converting smart contracts into semantically rigorous formal models that can be used in model checking methods still face the challenges of poor usability and difficulty in breaking away from manual modeling. Colored Petri nets, as discrete state-based systems, have similarities to smart contracts and are suitable for analyzing interactions between transactions. The analysis of control flow and data flow interactions, and transactions on the blockchain is missing in the research on converting smart contracts into colored Petri nets. In this paper, we propose an automated modeling method based on colored Petri nets, using template modeling and combination with data flow interactions and transaction modeling. Firstly, the data and control flows are modeled and combined, and secondly, the external user invocation is modeled to be able to correctly portray the on-chain contract invocations. The correctness in the smart contract is then verified based on the colored Petri net. Finally a prototype tool is implemented to demonstrate the usability and correctness of the modeling algorithm.