Title :
Formal analysis of the priority ceiling protocol
Author_Institution :
Syst. Design Lab., SRI Int., France
Abstract :
We present a case study in formal specification and tool-assisted verification of real-time schedulers, based on the priority ceiling protocol. Starting from operational specifications of the protocol, we obtain rigorous proofs of both synchronization and timing properties, and we derive a schedulability result for sporadic tasks
Keywords :
formal specification; program verification; protocols; real-time systems; scheduling; case study; formal specification; priority ceiling protocol; real-time schedulers; schedulability; sporadic tasks; synchronization; timing; tool-assisted verification; Contracts; Formal specifications; Laboratories; Mechanical factors; Operating systems; Protocols; Real time systems; System analysis and design; System recovery; Timing;
Conference_Titel :
Real-Time Systems Symposium, 2000. Proceedings. The 21st IEEE
Conference_Location :
Orlando, FL
Print_ISBN :
0-7695-0900-2
DOI :
10.1109/REAL.2000.896005
