A Foundation for Formally Proven Schedulability Analysis

What is Prosa?

Prosa is a repository of definitions and proofs for mechanized (i.e., machine-checkable) real-time schedulability analysis. To ensure full correctness, Prosa is built and verified with the Rocq prover, 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:

• Check out the overview of results for a list of the main high-level theorems that have been formalized and verified in Prosa to date.

• Learn why (and which) real-time scheduling theory should be mechanized.

• See the original Prosa paper for an in-depth discussion of the project’s motivation and goals, and Bedarkar et al.’s more recent case study for a detailed step-by-step guide to proving a response-time bound with modern Prosa.

• To simply run some of the verified analyses found in Prosa without getting into Rocq proofs yourself, check out the POET RTA tool and the underlying pyRTA library for response-time analysis in Python.

• To see how Prosa can be applied to real, running systems implemented in the C programming language, check out Bedarkar et al.’s RefinedProsa approach.

Why should I use Prosa?

Prosa is a framework for developing schedulability analysis backed by mechanized proofs, i.e., formal proofs that are developed and checked using the Rocq proof assistant. The mechanization process provides three main benefits:

• Guaranteed correctness: since proofs are machine-checked, they are bug-free and can be easily checked by third parties.

• Trustworthy extensions: localized changes in the task model (e.g., to introduce jitter, blocking, or system overheads) or other assumptions can be factored in systematically, without compromising correctness. If a change in assumptions breaks a proof, it will be flagged by the proof assistant.

• Safe composition: schedulability analyses that are individually correct can be safely composed without the risk of implicit or mismatching assumptions. In Prosa, all assumptions are explicit, and attempts to use theorems with the “wrong” assumptions will be flagged by the proof assistant.

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.