article · 1999

The Priority Ceiling Protocol: Formalization and Analysis Using PVS

Bruno Dutertre

Cited by 0Abstract and details only

Abstract

Common real-time operating systems rely on priority-based, preemptive scheduling. Re-source 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 mech-anism. 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. Chapter 1

Cite this paper

APA 7

Dutertre, B. (1999). The Priority Ceiling Protocol: Formalization and Analysis Using PVS.

MLA 9

Dutertre, Bruno. “The Priority Ceiling Protocol: Formalization and Analysis Using PVS.” 1999.

Chicago

Dutertre, Bruno. 1999. “The Priority Ceiling Protocol: Formalization and Analysis Using PVS.”

Harvard

Dutertre, B. (1999) ‘The Priority Ceiling Protocol: Formalization and Analysis Using PVS’.

BibTeX

@article{dutertre1999priority,
  title = {{The Priority Ceiling Protocol: Formalization and Analysis Using PVS}},
  author = {Dutertre, Bruno},
  year = {1999}
}

Made from the index record. Check names, capitalisation and page numbers against the paper. Need another style? AI for Research has over 10,000.