Document Open Access Logo

Automatic Code and Test Generation of Smart Contracts from Coordination Models

Authors Elvis Konjoh Selabi , Maurizio Murgia , António Ravara , Emilio Tuosto

PDF

File

Thumbnail PDF
PDF
LIPIcs.ECOOP.2026.15.pdf
  • Filesize: 2.09 MB
  • 30 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal methods
  • Theory of computation → Program semantics
  • Software and its engineering → Domain specific languages
Keywords
  • Smart Contracts
  • Coordination Models
  • Formal Semantics
  • Role-Based Access
  • Decentralised Systems
  • Code Generation
  • Solidity
  • Verification

Metrics

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.

Cite As Get BibTex

Elvis Konjoh Selabi, Maurizio Murgia, António Ravara, and Emilio Tuosto. Automatic Code and Test Generation of Smart Contracts from Coordination Models. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 15:1-15:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.ECOOP.2026.15

Author Details

Elvis Konjoh Selabi
  • Università di Camerino, Italy
  • Gran Sasso Science Institute, L'Aquila, Italy
Maurizio Murgia
  • Gran Sasso Science Institute, L'Aquila, Italy
António Ravara
  • NOVA School of Science and Technology, Almada, Portugal
Emilio Tuosto
  • Gran Sasso Science Institute, L'Aquila, Italy

Funding

  • Murgia, Maurizio: The MUR "dipartimento di eccellenza".
  • Ravara, António: Supported by FCT (Fundação para a Ciência e a Tecnologia) through the project NOVA LINCS (UID/04516/2025, https://doi.org/10.54499/UID/04516/2025).
  • Tuosto, Emilio: The MUR "dipartimento di eccellenza".

Supplementary Materials

References

  1. João Afonso, Elvis Konjoh Selabi, Maurizio Murgia, António Ravara, and Emilio Tuosto. TRAC: A Tool for Data-Aware Coordination (with an Application to Smart Contracts). In Proceedings of the 26th IFIP WG 6.1 International Conference on Coordination Models and Languages (COORDINATION), Held as Part of the 19th International Federated Conference on Distributed Computing Techniques (DisCoTec), pages 239-257. Springer-Verlag, 2024. URL: https://doi.org/10.1007/978-3-031-62697-5_13.
  2. Issam Al-Azzoni, Reiko Heckel, and Zobia Erum. Dynamic role-based access control scenarios for smart contracts: Graph rewriting for testing domain-specific models. J. Object Technol., 24(2):2, 2025. URL: https://doi.org/10.5381/JOT.2025.24.2.A4.
  3. Nicola Atzei, Massimo Bartoletti, and Tiziana Cimoli. A survey of attacks on Ethereum smart contracts (SoK). In POST, volume 10204 of LNCS, pages 164-186. Springer, 2017. URL: https://doi.org/10.1007/978-3-662-54455-6_8.
  4. Christel Baier, Marjan Sirjani, Farhad Arbab, and Jan J. M. M. Rutten. Modeling component connectors in reo by constraint automata. Sci. Comput. Program., 61(2):75-113, 2006. URL: https://doi.org/10.1016/J.SCICO.2005.10.008.
  5. Morena Barboni, Andrea Morichetta, and Andrea Polini. Sumo: A mutation testing strategy for Solidity smart contracts. In Proceedings of the 2021 IEEE/ACM International Conference on Automation of Software Test (AST), pages 50-59, 2021. URL: https://doi.org/10.1109/AST52587.2021.00014.
  6. Morena Barboni, Andrea Morichetta, Andrea Polini, and Francesco Casoni. ReSuMo: a regression strategy and tool for mutation testing of Solidity smart contracts. Software Quality Journal, 32(1):225-253, 2023. URL: https://doi.org/10.1007/s11219-023-09637-1.
  7. Massimo Bartoletti, Letterio Galletta, and Maurizio Murgia. A minimal core calculus for solidity contracts. In Cristina Pérez-Solà, Guillermo Navarro-Arribas, Alex Biryukov, and Joaquín García-Alfaro, editors, Data Privacy Management, Cryptocurrencies and Blockchain Technology - ESORICS 2019 International Workshops, Proceedings, Lecture Notes in Computer Science, pages 233-243. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-31500-9_15.
  8. Ananda Basu, Bensalem Bensalem, Marius Bozga, Jacques Combaz, Mohamad Jaber, Thanh-Hung Nguyen, and Joseph Sifakis. Rigorous Component-Based System Design Using the BIP Framework. IEEE Software, 28:41-48, 2011. URL: https://doi.org/10.1109/MS.2011.27.
  9. Rajendra Bisoi. Simple Wallet Smart Contract. https://github.com/coderRaj07/Simple-Wallet-Smart-Contract, 2022. Accessed: 2025.
  10. Sam Blackshear, Evan Cheng, David L. Dill, Victor Gao, Ben Maurer, Todd Nowacki, Alistair Pott, Shaz Qadeer, Rain, Dario Russi, Stephane Sezer, Tim Zakian, and Runtian Zhou. Move: A Language with Programmable Resources. https://developers.diem.com/docs/technical-papers/move-paper/, 2019. White paper, Libra Association.
  11. Chiara Braghin, Giuseppe Del Castillo, Elvinia Riccobene, and Simone Valentini. Using symbolic model execution to detect vulnerabilities of smart contracts. In Michael Leuschel and Fuyuki Ishikawa, editors, Rigorous State-Based Methods - 11th International Conference, ABZ 2025, Düsseldorf, Germany, June 10-13, 2025, Proceedings, volume 15728 of Lecture Notes in Computer Science, pages 31-51. Springer, 2025. URL: https://doi.org/10.1007/978-3-031-94533-5_3.
  12. Chiara Braghin, Elvinia Riccobene, and Simone Valentini. Modeling and verification of smart contracts with abstract state machines. In Jiman Hong and Juw Won Park, editors, Proceedings of the 39th ACM/SIGAPP Symposium on Applied Computing, SAC 2024, Avila, Spain, April 8-12, 2024, pages 1425-1432. ACM, 2024. URL: https://doi.org/10.1145/3605098.3636040.
  13. Alessandro Cimatti, Edmund Clarke, Fausto Giunchiglia, and Marco Roveri. NuSMV: A new symbolic model verifier. In International conference on computer aided verification, pages 495-499. Springer, 1999. URL: https://doi.org/10.1007/s100090050046.
  14. Hubert Comon and Yan Jurski. Multiple counters automata, safety analysis and presburger arithmetic. In Alan J. Hu and Moshe Y. Vardi, editors, Computer Aided Verification, 10th International Conference, CAV '98, Vancouver, BC, Canada, June 28 - July 2, 1998, Proceedings, volume 1427 of Lecture Notes in Computer Science, pages 268-279. Springer, 1998. URL: https://doi.org/10.1007/BFB0028751.
  15. Flavio Corradini, Alessandro Marcelletti, Andrea Morichetta, Andrea Polini, Barbara Re, and Francesco Tiezzi. Engineering Trustable and Auditable Choreography-based Systems Using Blockchain. ACM Transactions on Management Information Systems, 13:31:1-31:53, 2022. URL: https://doi.org/10.1145/3505225.
  16. Flavio Corradini, Alessandro Marcelletti, Andrea Morichetta, Andrea Polini, Barbara Re, and Francesco Tiezzi. Blockchain-based Execution of BPMN Choreographies with Multiple Instances. Distributed Ledger Technologies: Research and Practice, 2023. URL: https://doi.org/10.1145/3637555.
  17. Silvia Crafa, Matteo Di Pirro, and Elena Zucca. Is solidity solid enough? In Andrea Bracciali, Jeremy Clark, Federico Pintore, Peter B. Rønne, and Massimiliano Sala, editors, Financial Cryptography and Data Security - FC 2019 International Workshops, VOTING and WTSC, Revised Selected Papers, Lecture Notes in Computer Science, pages 138-153. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-43725-1_11.
  18. Massimiliano de Leoni, Paolo Felli, and Marco Montali. A Holistic Approach for Soundness Verification of Decision-Aware Process Models. In Juan Trujillo, Karen C. Davis, Xiaoyong Du, Zhanhuai Li, Tok Wang Ling, Guoliang Li, and Mong-Li Lee, editors, Proceedings of the 37th International Conference on Conceptual Modeling (ER), volume 11157 of Lecture Notes in Computer Science, pages 219-235. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-00847-5_17.
  19. Leonardo de Moura and Nikolaj Bjørner. Z3: An Efficient SMT Solver. In Proceedings of the Internatioanl Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 337-340. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78800-3_24.
  20. Stefan Driessen, Dario Di Nucci, Geert Monsieur, and Willem-Jan van den Heuvel. AGSolT: a Tool for Automated Test-Case Generation for Solidity Smart Contracts. CoRR, abs/2102.08864, 2021. URL: https://arxiv.org/abs/2102.08864.
  21. Jinhu Du, Song Huang, Xingya Wang, Changyou Zheng, and Jinlei Sun. Test Case Generation for Ethereum Smart Contract based on Data Dependency Analysis of State Variable. In Proceedings of the IEEE 22nd International Conference on Software Quality, Reliability and Security (QRS), pages 710-720, 2022. URL: https://doi.org/10.1109/QRS57517.2022.00077.
  22. Mojtaba Eshghie, Wolfgang Ahrendt, Cyrille Artho, Thomas Troels Hildebrandt, and Gerardo Schneider. Capturing smart contract design with DCR graphs. In Carla Ferreira and Tim A. C. Willemse, editors, Software Engineering and Formal Methods - 21st International Conference, SEFM 2023, Eindhoven, The Netherlands, November 6-10, 2023, Proceedings, Lecture Notes in Computer Science, pages 106-125. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-47115-5_7.
  23. Mojtaba Eshghie, Cyrille Artho, Hans Stammler, Wolfgang Ahrendt, Thomas T. Hildebrandt, and Gerardo Schneider. Highguard: Cross-chain business logic monitoring of smart contracts. In Vladimir Filkov, Baishakhi Ray, and Minghui Zhou, editors, Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering, ASE 2024, Sacramento, CA, USA, October 27 - November 1, 2024, pages 2378-2381. ACM, 2024. URL: https://doi.org/10.1145/3691620.3695356.
  24. Nomic Foundation. Hardhat 3: Rust-powered Solidity Tests, 2025. Google Scholar
  25. Christopher K Frantz and Mariusz Nowostawski. From institutions to code: Towards automated generation of smart contracts. In 2016 IEEE 1st International Workshops on Foundations and Applications of Self* Systems (FAS* W), pages 210-215. IEEE, 2016. URL: https://doi.org/10.1109/FAS-W.2016.53.
  26. Ronald Garcia, Éric Tanter, Roger Wolff, and Jonathan Aldrich. Foundations of Typestate-Oriented Programming. ACM Transactions on Programming Languages and Systems, 36:12, 2014. URL: https://doi.org/10.1145/2629609.
  27. Simon Gay and António Ravara. Behavioural Types: from Theory to Tools. River Publishers, 2017. URL: https://doi.org/10.1201/9781003337331.
  28. David Gelernter. Generative Communication in Linda. ACM Transactions on Programming Languages and Systems, 7:80-112, 1985. URL: https://doi.org/10.1145/2363.2433.
  29. Javier Godoy, Juan Pablo Galeotti, Diego Garbervetsky, and Sebastián Uchitel. Predicate Abstractions for Smart Contract Validation. In Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems (MODELS), pages 289-299, 2022. URL: https://doi.org/10.1145/3550355.3552462.
  30. Gustavo Grieco, Will Song, Artur Cygan, Josselin Feist, and Alex Groce. Echidna: effective, usable, and fast fuzzing for smart contracts. In Proceedings of the 29th ACM SIGSOFT international symposium on software testing and analysis, pages 557-560, 2020. URL: https://doi.org/10.1145/3395363.3404366.
  31. Mohammad Hamdaqa, Lucas Alberto Pineda Metz, and Ilham Qasse. iContractML 2.0: A domain-specific language for modeling and deploying smart contracts onto multiple blockchain platforms. Information and Software Technology, 144, 2022. URL: https://doi.org/10.1016/j.infsof.2021.106762.
  32. Wen-ling Huang, Niklas Krafczyk, and Jan Peleska. Exhaustive property oriented model-based testing with symbolic finite state machines. Sci. Comput. Program., 231:103005, 2024. URL: https://doi.org/10.1016/J.SCICO.2023.103005.
  33. Mantas Jurgelaitis, Lina Čeponienė, and Rita Butkienė. Solidity Code Generation from UML State Machines in Model-Driven Smart Contract Development. IEEE Access, 10:33465-33481, 2022. URL: https://doi.org/10.1109/ACCESS.2022.3162227.
  34. Elvis KONJOH SELABI, Maurizio Murgia, António Ravara, and Emilio Tuosto. Automatic Code and Test Generation of Smart Contracts from Coordination Models (Artifact), February 2026. URL: https://doi.org/10.5281/zenodo.18475933.
  35. Ye Liu, Yi Li, Shang-Wei Lin, and Qiang Yan. Modcon: a model-based testing platform for smart contracts. In Prem Devanbu, Myra B. Cohen, and Thomas Zimmermann, editors, Proceedings of the ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE), pages 1601-1605, 2020. URL: https://doi.org/10.1145/3368089.3417939.
  36. Hugo A. López and Thomas T. Hildebrandt. Three decades of formal methods in business process compliance: A systematic literature review, 2024. URL: https://doi.org/10.48550/arXiv.2410.10906.
  37. Felix Mannhardt, Massimiliano De Leoni, Hajo A Reijers, and Wil M. P. Van Der Aalst. Balanced multi-perspective checking of process conformance. Computing, 98:407-437, 2016. URL: https://doi.org/10.1007/S00607-015-0441-1.
  38. Anastasia Mavridou and Aron Laszka. Designing Secure Ethereum Smart Contracts: A Finite State Machine Based Approach. In Proceedings of the 22nd International Conference on Financial Cryptography and Data Security (FC), volume 10957 of Lecture Notes in Computer Science, pages 523-540. Springer, 2018. URL: https://doi.org/10.1007/978-3-662-58387-6_28.
  39. Anastasia Mavridou, Aron Laszka, Emmanouela Stachtiari, and Abhishek Dubey. VeriSolid: Correct-by-Design Smart Contracts for Ethereum. In Proceedings of the 23rd International Conference on Financial Cryptography and Data Security (FC), volume 11598 of Lecture Notes in Computer Science, pages 446-465. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-32101-7_27.
  40. Sun Meng and Farhad Arbab. Web Services Choreography and Orchestration in Reo and Constraint Automata. In Proceedings of the 2007 ACM symposium on Applied computing, pages 346-353, 2007. URL: https://doi.org/10.1145/1244002.1244085.
  41. Microsoft. Simple Marketplace Sample Application for Azure Blockchain Workbench, 2019. Google Scholar
  42. Microsoft. The Blockchain Workbench, 2019. URL: https://github.com/Azure-Samples/blockchain/tree/master/blockchain-workbench/application-and-smart-contract-samples.
  43. Mikkel Milo, Eske Hoy Nielsen, Danil Annenkov, and Bas Spitters. Finding Smart Contract Vulnerabilities with ConCert’s Property-Based Testing Framework. In Zaynah Dargaye and Clara Schneidewind, editors, 4th International Workshop on Formal Methods for Blockchains (FMBC 2022), volume 105 of Open Access Series in Informatics (OASIcs), pages 2:1-2:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/OASIcs.FMBC.2022.2.
  44. Gero Mühl, Ludger Fiege, and Peter Pietzuch. Distributed Event-Based Systems. Springer Science & Business Media, 2006. Google Scholar
  45. Wander Nauta, Marcus Gerhold, and Marieke Huisman. Crash-free deductive verifiers. In SPIN 2026 (to appear), 2026. Google Scholar
  46. Keerthi Nelaturu, Anastasia Mavridou, Emmanouela Stachtiari, Andreas Veneris, and Aron Laszka. Correct-by-Design Interacting Smart Contracts and a Systematic Approach for Verifying ERC20 and ERC721 Contracts With VeriSolid. IEEE Transactions on Dependable and Secure Computing, 20(4):3110-3127, 2023. URL: https://doi.org/10.1109/TDSC.2022.3200840.
  47. Oscar Nierstrasz. Regular Types for Active Objects. ACM SIGPLAN Notices, 28:1-15, 1993. URL: https://doi.org/10.1145/167962.167976.
  48. OpenZeppelin. OpenZeppelin Contracts: A Library for Secure Smart Contract Development, 2025. Google Scholar
  49. OpenZeppelin. OpenZeppelin Test Suite for ERC20. https://github.com/OpenZeppelin/openzeppelin-contracts/tree/master/test/token/ERC20, 2025.
  50. Michael Papazoglou. Web Services and SOA: Principles and Technology. Pearson Education Limited, 2012. Google Scholar
  51. Chris Peltz. Web services orchestration and choreography. IEEE Computer, 36(10):46-52, 2003. URL: https://doi.org/10.1109/MC.2003.1236471.
  52. Andrei Permenev, Petar Tsankov, Dana Drachsler-Cohen, Seif Haridi, and David Basin. VerX: Safety Verification of Smart Contracts. In Proceedings of the IEEE Symposium on Security and Privacy (S&P), pages 1661-1677, 2020. Google Scholar
  53. Rootstrap. How to Create Your Own DeFi AMM - Easy Guide. https://www.rootstrap.com/blog/how-to-create-your-own-defi-amm-easy-guide, 2023. Accessed: 2025-05-27.
  54. Elvis Konjoh Selabi, Maurizio Murgia, António Ravara, and Emilio Tuosto. Automatic code and test generation of smart contracts from coordination models, 2026. URL: https://doi.org/10.48550/arXiv.2604.20507.
  55. Frank Siqueira and Joseph G. Davis. Service computing for industry 4.0: State of the art, challenges, and research opportunities. ACM Computing Surveys, 54(9), 2021. URL: https://doi.org/10.1145/3478680.
  56. R. E. Strom and S. Yemini. Typestate: A Programming Language Concept for Enhancing Software Reliability. IEEE Transactions on Software Engineering, SE-12:157-171, 1986. URL: https://doi.org/10.1109/TSE.1986.6312929.
  57. Konstantinos Tsiounis and Kostas Kontogiannis. Goal Driven Code Generation for Smart Contract Assemblies. In Proceedings of the 2023 12th International Conference on Software and Computer Applications, pages 112-121, 2023. URL: https://doi.org/10.1145/3587828.3587846.
  58. Fabian Vogelsteller and Vitalik Buterin. ERC-20 Token Standard. https://ethereum.org/en/developers/docs/standards/tokens/erc-20/, 2025. Accessed: 2025-05-27.
  59. Zhiyuan Wei, Jing Sun, Zijian Zhang, Xianhao Zhang, Xiaoxuan Yang, and Liehuang Zhu. Survey on quality assurance of smart contracts. ACM Comput. Surv., 57(2):32:1-32:36, 2025. URL: https://doi.org/10.1145/3695864.
  60. Jiashuo Zhang, Jiachi Chen, John Grundy, Jianbo Gao, Yanlin Wang, Ting Chen, Zhi Guan, and Zhong Chen. Automated Test Generation for Smart Contracts via On-Chain Test Case Augmentation and Migration. In Proceedings of the ACM/IEEE International Conference on Software Engineering (ICSE), 2025. URL: https://ieeexplore.ieee.org/document/11029866.
  61. Tilman Zuckmantel, Yongluan Zhou, Boris Düdder, and Thomas T. Hildebrandt. DACEO: declarative asynchronous choreographies with general data-dependent event-ordering and objects. In Cinzia Di Giusto and António Ravara, editors, Coordination Models and Languages - 27th IFIP WG 6.1 International Conference, COORDINATION 2025, Held as Part of the 20th International Federated Conference on Distributed Computing Techniques, DisCoTec 2025, Lille, France, June 17-19, 2025, Proceedings, Lecture Notes in Computer Science, pages 197-216. Springer, 2025. URL: https://doi.org/10.1007/978-3-031-95589-1_10.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact