DocumentCode
2785593
Title
Formal analysis of the priority ceiling protocol
Author
Dutertre, Bruno
Author_Institution
Syst. Design Lab., SRI Int., France
fYear
2000
fDate
2000
Firstpage
151
Lastpage
160
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Real-Time Systems Symposium, 2000. Proceedings. The 21st IEEE
Conference_Location
Orlando, FL
ISSN
1052-8725
Print_ISBN
0-7695-0900-2
Type
conf
DOI
10.1109/REAL.2000.896005
Filename
896005
Link To Document