Automatic Code and Test Generation of Smart Contracts from Coordination Models
This work addresses the challenge of formalizing and automating smart contract development for blockchain platforms, with potential generalization to other distributed architectures, but it is incremental as it builds on existing coordination models.
The authors tackled the problem of specifying and implementing decentralized coordination in distributed systems, particularly for smart contracts, by developing a formal model and toolchain that enables model validation, Solidity code generation, and automated test synthesis, demonstrating its expressiveness and practicality with coordination patterns.
We propose a formal approach for specifying and implementing decentralised coordination in distributed systems, with a focus on smart contracts. Our model captures dynamic roles, data-driven transitions, and external coordination interfaces, enabling high-level reasoning about decentralised workflows. We implement a toolchain that supports formal model validation, code generation for Solidity (our framework is extendable to other smart contract languages), and automated test synthesis. Although our implementation targets blockchain platforms, the methodology is platform-agnostic and may generalise to other service-oriented and distributed architectures. We demonstrate the expressiveness and practicality of the approach by modelling and realising some coordination patterns in smart contracts.