A heterogeneous swarm system is a distributed system where participants come and go, communication topology may change at any time, data replication is asynchronous and partial, and local agents behave differently between nodes. These systems are hard to design and reason about, mainly because we desire a particular class of behaviors to emerge from the interplay of heterogeneous individual agents. Nevertheless, mission-critical operations like manufacturing process orchestration in factories use such systems due to their uncompromising availability and resilience of computing services. This paper presents a set of TypeScript libraries to model peer-to-peer workflows as state machines, execute them using the Actyx middleware, and check the shape of these machines for conformance to a swarm protocol. The swarm protocol describes an idealized global view of the cooperation of machines of different roles. It directly corresponds to a diagram a product manager would sketch on a whiteboard; this allows for verifying that the coded state machines correctly implement the product specification. A well-formed swarm protocol also guarantees that conforming machines will achieve eventual consensus on the overall state progression even in the absence of further coordination. This tool is for developers of business logic for heterogeneous swarm systems, helping them verify that their protocols and implementations are correct. Tool repo: https://github.com/Actyx/machines

@inproceedings{KuhnD23,
  title = {Behaviorally Typed State Machines in TypeScript for Heterogeneous Swarms},
  author = {Roland Kuhn and Alan Darmasaputra},
  booktitle = {ISSTA},
  year = {2023},
  doi = {10.1145/3597926.3604917}
}