Compositional Verification of a Distributed
Real-Time Arbitration Protocol
Jozef Hooman
Appeared in: Real-Time Systems, Volume 6, Number 2, pages 173-205, 1994.
ABSTRACT
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.
Postscript