A specification language for coordinated objects

The paper presents a specification language of autonomous objects supervised by a coordinating process. The coordination is defined by means of an interaction wrapper. The coordination semantics is described in the terms of bisimulation relations. The properties of the coordinated objects are expressed as temporal formulas, and verified by specific model-checking algorithms. We use the alternating bit protocol to exemplify our specification language and its semantics.This approach allows a clear separation of concerns: the same coordinating process can be used with different concurrent objects, and the same objects can be used with a different coordinator. Thus our specification language allows easy modifications and customization. The method is effective in assembling increasingly complex systems from components. Moreover, composing different coordinating processes can be done without changing the code of the coordinated objects. In this way, the difficult task of implementing the mechanism of coordination becomes substantially easier.