Compositional verification of a distributed real-time arbitration protocol

A distributed real-time arbitration protocol is specified and verified using an assertional method. The formalism is based on classical Hoare triples which have been extended to deal with real-time properties. To verify design steps, a compositional proof system has been formulated for these extended triples. The intention of the protocol is to resolve contention between a number of concurrent modules that compete to acquire control of a common bus. Therefore our proof method has been adapted to deal with concurrent processes that communicate by means of a common bus. Compositionality makes it possible to verify the required properties of the protocol using only the specifications of the modules. Next we give a top-down derivation of a program implementing a module according to its real-time specification.