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:
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.
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.
To simply run some of the verified analyses found in Prosa without getting into Coq yourself, check out the POET RTA tool.
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:
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 any differences in 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.
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.
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.