Model-Based Testing Approach for EIP-1559 Ethereum Smart Contracts

Smart contracts are computer programs that are deployed and executed on the blockchain without the need of third parties. They are characterized by their immutability because once deployed, they cannot be modified. Thus, it is highly demanded to verify and validate them at development phase before their deployment. This work introduces a Model-Based Testing (MBT) approach for checking functional and execution related properties of Ethereum smart contracts. Our MBT solution supports the transaction pricing mechanism set by the Ethereum Improvement Proposal EIP-1559. It consists of four steps: (1) modelling the smart contract and its blockchain environment as UPPAAL Timed Automata while defining the contract gas usage regarding the EIP-1559 proposal, (2) generating abstract test cases, (3) executing dynamically the obtained tests, and at the end (4) analyzing and reporting the obtained test results. To illustrate the feasibility of our MBT approach, tests for the smart banking case study are generated and executed.