Prosa is a repository of definitions and proofs for real-time schedulability analysis. To ensure full correctness, Prosa is built and and mechanically verified with Coq, a powerful and mature proof assistant with support for higher-order logic and computations. Prosa’s distinguishing characteristic is that **Prosa prioritizes readability** over all other concerns to ensure that specifications remain *accessible* to readers without a background in formal proofs. (A background in real-time scheduling is assumed.)

See the Prosa paper for an in-depth introduction.

**July 2020**: Bozhko and Brandenburg win an**Outstanding Paper Award**at ECRTS’20 for their paper on abstract response-time analysis in Prosa — check it out (PDF).**December 2019**: Prosa 0.4 released, a completely refactored version of Prosa.**October 2019**: Fourth RT-PROOFS meeting @ Inria in Paris, France.**July 2019**: New paper by Guo et al. on a connection between CertiKOS and Prosa — check it out (PDF).**June 2019**: Up-to-date coqdoc documentation for the master branch and work-in-progress branches is now available at https://prosa.mpi-sws.org/branches.**April 2019**: New paper by Fradet et al. on CertiCAN, a tool for certified CAN analysis — check it out (PDF).**April 2019**: Third RT-PROOFS meeting @ TUBS in Braunschweig, Germany.**December 2018**: New paper by Fradet et al. on a generic proof of typical worst-case analysis at RTSS’18 — check it out (PDF).**October 2018**: New paper by Fradet et al. on generalized digraph models at RTNS’18 — check it out (PDF).**September 2018**: Second RT-PROOFS meeting @ MPI-SWS in Kaiserslautern, Germany.**July 2018**: Prosa 0.3 released, including a formalization of sustainability theory and self-suspending tasks.**July 2018**: New work-in-progress paper by Riffard et al. on support for synchronization protocols in Prosa — check it out (PDF)!**July 2018**: Cerqueira et al. win an**Outstanding Paper Award**at ECRTS’18 for their paper on strong and weak sustainability, with proofs checked in Prosa — check it out (PDF)!**January 2018**: First RT-PROOFS meeting @ ONERA in Toulouse, France.**December 2017**: New work-in-progress paper by Xiaojie Guo et al. on certified schedulability analysis tools — check it out (PDF)!**October 2017**: The French-German RT-PROOFS project, which leverages and seeks to improve Prosa, is funded by ANR and DFG for three years (≈660k EUR).**July 2016**: Cerqueira et al. win the**ECRTS’16 Best Paper Award**for their paper introducing Prosa.**June 2016**: Prosa 0.2 released, with support for arbitrary processor affinities (APA).**May 2016**: Prosa 0.1 released.

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 *definitions*, *hypotheses*, and *theorems*, with extensive commentary in between. To provide a taste of what it looks like, we provide a short example of a simple lemma. For the sake of brevity, we don’t provide the full context of the specification.

**Example:** *Assume that jobs are sequential, i.e., any single job cannot be scheduled on multiple processors in parallel.*

**Explanation:** this fragment introduces an assumption, named `H_sequential_jobs`

for later reference, that states that, in any considered schedule `sched`

(defined previously in the context, not shown here), all jobs execute sequentially (with the `sequential_jobs`

predicate, definition not shown here). In Prosa, all assumptions are made explicitly using this `Hypothesis`

syntax, which greatly aids readability.

*Then, let #j# be any job in the arrival sequence.*

**Explanation:** this fragment introduces a new variable, named `j`

, to denote an arbitrary job of a sporadic task. The type of the variable is `JobIn arr_seq`

, which means that job `j`

stems from the arrival sequence `arr_seq`

, where `arr_seq`

is an arbitrary legal arrival sequence (definition not shown here).

*Using the job sequentiality assumption, we prove that the instantaneous service received by job #j# at any time #t# is at most one time unit.*

(* The service received by any job j at any time t is at most 1. *)

Lemma service_at_most_one :

∀ t, service_at sched j t ≤ 1.

Lemma service_at_most_one :

∀ t, service_at sched j t ≤ 1.

[Show Proof]

**Explanation:** there are two parts to this fragment. The first part is the **lemma statement** (i.e., the claim). In Prosa, lemma claims are kept intentionally simple to make sure that they can be understood without a deep knowledge of Coq. For instance, in this example, the lemma quite literally states that, at any time `t`

, the job `j`

receives at most one time unit of processor service, which follows from the assumption that jobs are sequential.

The second part is the *justification* of the claim, which is a low-level *proof script* that instructs Coq how to construct a **formal proof** (technically, a *proof term*) for the claim. In contrast to the specification (definitions and claims), *proof scripts are not intended for human consumption* and require significant Coq expertise (and use of the proof assistant) to be understood.

This highlights the Prosa goals and principles:

the specification and claims should be accessible to, and understood by, anyone with a background in real-time scheduling, whereas

the development of new proofs is necessarily a task that requires more specialized Coq knowledge.

However, even *non-experts can easily verify that the provided proofs are correct* by downloading Prosa and running the Coq proof checker.

For a gentle introduction to Prosa and the use of mechanized proofs for schedulability analysis, please check out the ECRTS’16 paper.

To learn more about how to read formal specifications in Prosa and how to develop formal proofs, please consult the getting started guide and the provided documentation.

If you have further questions, please don’t hesitate to send a message to our mailing list.