Automatic Code and Test Generation of Smart Contracts from Coordination Models

TL;DR

This paper introduces a formal method and toolchain for specifying, validating, and generating smart contract code and tests from high-level coordination models, enhancing decentralised workflow development.

Contribution

It presents a novel formal approach and extendable toolchain for automatic code and test generation of smart contracts from coordination models.

Findings

Successfully modeled and implemented coordination patterns in smart contracts.

Demonstrated the expressiveness and practicality of the approach.

Framework supports formal validation and automated test synthesis.

Abstract

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.