DocumentCode
2601227
Title
Specification and verification of a distributed real-time arbitration protocol
Author
Hooman, Jozef
Author_Institution
Dept. of Math. & Comput. Sci., Eindhoven Univ. of Technol., Netherlands
fYear
1993
fDate
1-3 Dec 1993
Firstpage
284
Lastpage
293
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Real-Time Systems Symposium, 1993., Proceedings.
Conference_Location
Raleigh Durham, NC
Print_ISBN
0-8186-4480-X
Type
conf
DOI
10.1109/REAL.1993.393488
Filename
393488
Link To Document