SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
  SRI Logo

The Priority Ceiling Protocol: Formalization and Analysis Using PVS
 by Dr. Bruno Dutertre.

Common real-time operating systems rely on priority-based, preemptive scheduling. Resource sharing in such systems potentially leads to priority inversion: processes of high priority can be prevented from entering a critical section and be delayed by processes of lower priority. Since uncontrolled priority inversion can cause high priority processes to miss their deadlines, a real-time operating system must use resource-sharing mechanisms that limit the effects of priority inversion. The priority ceiling protocol is one such mechanism. It ensures mutual exclusion and absence of deadlocks, and minimizes the length of priority inversion periods. This paper presents a formal specification and analysis of the protocol using PVS and the rigorous proof of associated schedulability results.


About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2023 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy