Synchronous Multi-Agent ASMs

Abstract

In this chapter¹ the single-agent ASMs of Chaps. 3, 4 are extended to multiagent synchronous ASMs (sync ASM) which support modularity for the design of large systems. We illustrate this by sync ASMs for two popular benchmark case studies for the verified design of reactive control systems: a controller for the Production Cell [323] (Sect. 5.1), solving a typical industrial plant control problem, and a real-time gate controller for the Generalized Railroad Crossing [277] (Sect. 5.2), both controllers coming with to- be-verified safety, liveness and performance requirements. Although the case studies are really small (leading to roughly 1 K lines of controller code), they allow us to explain how to apply practically useful software architecture principles to modularize systems, starting from ground model ASMs and leading to verified code. The chapter can be read independently of the preceding Chaps. 4 and 3 and most of Chap. 2; it suffices to know the definition of basic ASMs and of ASM refinements.