Swarm protocols are a recently introduced formalism for specifying, implementing, and verifying peer-to-peer systems called swarms. A swarm consists of distributed agents called machines that communicate by asynchronous event propagation. Following a local-first model, each machine can progress without requiring continuous connectivity to other machines. Existing models of swarms are not compositional, making the modular development of large and complex swarm applications as well as the reuse of code difficult. We address these issues by presenting novel theory and techniques for the compositional specification, verification, and implementation of swarms. These results enable the correct compositional reuse of pre-existing swarm protocols and machine implementations. We implement these contributions in a companion software artifact which enables the automatic integration of independently designed and verified swarm components.

翻译：群组协议是一种近期提出的形式化框架，用于描述、实现和验证称为群组的对等系统。一个群组由称为机器的分布式代理组成，这些代理通过异步事件传播进行通信。遵循本地优先模型，每台机器无需与其他机器保持持续连接即可推进计算。现有群组模型缺乏组合性，导致难以模块化开发大规模复杂群组应用，且代码重用困难。我们通过提出新型理论与技术来解决上述问题，这些成果涵盖群组的组合式规范、验证与实现，能够实现预存群组协议与机器实现的正确组合式复用。我们将这些贡献实现为配套软件工具，支持独立设计与验证的群组组件自动集成。