Title :
Specification and verification of a distributed real-time arbitration protocol
Author_Institution :
Dept. of Math. & Comput. Sci., Eindhoven Univ. of Technol., Netherlands
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
Keywords :
distributed processing; formal specification; formal verification; program verification; protocols; real-time systems; Hoare triples; common bus; compositional proof method; concurrent modules; distributed real-time arbitration protocol; distributed real-time systems; liveness properties; safety; specification; verification; Distributed computing; Explosions; Mathematics; Message passing; Parallel processing; Processor scheduling; Protocols; Real time systems; Safety; Timing;
Conference_Titel :
Real-Time Systems Symposium, 1993., Proceedings.
Conference_Location :
Raleigh Durham, NC
Print_ISBN :
0-8186-4480-X
DOI :
10.1109/REAL.1993.393488
