Asynchronous Multi-Agent ASMs

Abstract

In this chapter¹ the single-agent (basic or turbo) ASMs of Chaps. 3 and 4 and the multi-agent synchronous ASMs of Chap. 5 are extended to asynchronous multi-agent ASMs and shown to be useful for the design and the analysis of distributed systems. In Sect. 6.1 we define async ASMs and illustrate them by characteristic distributed network algorithms (for consensus, master—slave agreement, leader election, phase synchronization, load balance, broadcast acknowledgment) and a position-based routing protocol for mobile ad hoc networks. In Sect. 6.2 we show async ASMs at work in a requirements capture case study for a small embedded system (Light Control). In Sect. 6.3 we use async ASMs to model and analyze two time-constrained algorithms which support fault tolerance for a distributed computing service, namely in Sect. 6.3.1 the modem and network communication protocol Kermit for correct file transfer, well-known from TCP/IP installations, and in Sect. 6.3.2 a Processor Group Membership protocol. In Sect. 6.4 we use the ASM refinement method to show — adopting Lamport’s famous mutual exclusion algorithm Bakery as an example — how time-constrained algorithms with “atomic actions” can naturally be turned in a provably correct way to reflect also the “real-time duration ” of actions. We show that it suffices to refine the global state view of atomic non-overlapping reads and writes in shared registers to a local state view of single agents whose overlapping reads and writes to the same location are governed by the constraints that async ASM runs impose on controlled, monitored and shared locations. Section 6.5 deals with event-driven ASMs. As a concrete illustration we model in Sect. 6.5.1 event-driven UML activity diagrams by async ASMs with turbo components and apply them for a compact one-page definition of an interpreter for Occam programs.