| | | | |
|

Formal Analysis of the Priority Ceiling Protocol
by Dr. Bruno Dutertre.
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.
Files
|
|
|