Abstract
To specify and verify distributed real-time systems, we use a formalism based on Hoare triples. The framework has been adapted to deal with safety as well as liveness properties, and a compositional proof method has been formulated. The formalism is applied to a distributed real-time arbitration protocol in which concurrent modules compete to get control over a common bus.
Original language | English |
---|---|
Title of host publication | Proceedings 14th IEEE Real-Time Systems Symposium (Raleigh Durham NC, USA, December 1-3, 1993) |
Publisher | Institute of Electrical and Electronics Engineers |
Pages | 284-293 |
Number of pages | 10 |
ISBN (Print) | 0-8186-4480-X |
DOIs | |
Publication status | Published - 1993 |