A Foundation for Formally Proven Schedulability Analysis

What is Prosa?

Prosa is a repository of definitions and proofs for real-time schedulability analysis. To ensure full correctness, Prosa is built and verified with Coq, a powerful and mature proof assistant with support for higher-order logic and computation.

Prosa’s distinguishing characteristic is that Prosa prioritizes readability to ensure that specifications remain accessible to readers without a background in formal proofs. (A background in real-time scheduling is assumed.)

To get started:

News

Why should I use Prosa?

Prosa is a framework for developing schedulability analysis backed by mechanized proofs, i.e., formal proofs that are developed using a proof assistant (e.g., Coq, Isabelle, Agda, etc.). The mechanization process provides three main benefits:

One of the distinguishing features of Prosa is its emphasis on making the specification readable and accessible to the community at large. In the long term, as the formal specification gains widespread acceptance by the real-time community, Prosa will allow us to develop schedulability analysis with the highest-possible degree of confidence, matching the requirements of safety-critical applications.

What does Prosa look like?

Prosa is nothing more than a collection of reusable definitions, hypotheses, and theorems, with extensive commentary in between. As a representative example, check out the formalization of Bedarkar et al.’s response-time analysis for FIFO scheduling, which is described in detail in their RTSS’22 paper.

Where can I learn more?

To learn about the original ideas and motivation behind Prosa, and generally the case for use of mechanized proofs for schedulability analysis, please check out the ECRTS’16 paper.

For a gentle introduction to the contemporary version of Prosa, refer to Bedarkar et al.’s case study.

To learn more about how to read Prosa’s formal specifications and how to develop formal proofs, please consult the references provided in the documentation.