Specification of coordinated objects and verification of their temporal properties

This paper presents a specification framework for coordinated objects. Coordination is described by a process. The integration of the concurrent objects and the coordinating process is given by a wrapper. Using an encoding into Maude, we extract a Kripke structure describing the behavior of the specified system, and verify its temporal properties. We use the alternating bit protocol to exemplify our specification framework, and SMV to verify its correctness.