2026-09-08T11:38:43Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:26111 2026-09-05T19:37:21Z ddc:004 open_access

Automatic Code and Test Generation of Smart Contracts from Coordination Models Konjoh Selabi, Elvis Murgia, Maurizio Ravara, António Tuosto, Emilio Smart Contracts Coordination Models Formal Semantics Role-Based Access Decentralised Systems Code Generation Solidity Verification 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Elvis Konjoh Selabi and Maurizio Murgia and António Ravara and Emilio Tuosto 2026 Is Part Of LIPIcs, Volume 372, 40th European Conference on Object-Oriented Programming (ECOOP 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ECOOP.2026.15 urn:nbn:de:0030-drops-261119 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.15 eng https://creativecommons.org/licenses/by/4.0/legalcode