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.

翻译：我们提出了一种形式化方法，用于在分布式系统中指定和实现去中心化协调，重点关注智能合约。我们的模型能够捕获动态角色、数据驱动转换以及外部协调接口，从而实现对去中心化工作流的高层级推理。我们实现了一个工具链，支持形式化模型验证、针对Solidity的代码生成（我们的框架可扩展至其他智能合约语言），以及自动化测试综合。尽管我们的实现以区块链平台为目标，但该方法论与平台无关，并可泛化至其他面向服务的分布式架构。我们通过对智能合约中的若干协调模式进行建模与实现，展示了该方法的表达能力和实用性。