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.
|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|
|Number of pages||10|
|Publication status||Published - 1993|