Compositional verification of a distributed real-time arbitration protocol

J.J.M. Hooman

Research output: Contribution to journalArticleAcademicpeer-review

16 Citations (Scopus)


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.
Original languageEnglish
Pages (from-to)173-205
Number of pages33
JournalReal-Time Systems
Issue number2
Publication statusPublished - 1994


Dive into the research topics of 'Compositional verification of a distributed real-time arbitration protocol'. Together they form a unique fingerprint.

Cite this