Compositional verification of a distributed real-time arbitration protocol |
| |
Authors: | Jozef Hooman |
| |
Affiliation: | (1) Department of Mathematics and Computing Science, Eindhoven University of Technology, P.O. Box 513, 5600 MB Eindhoven, The Netherlands |
| |
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. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|