Prosa is a repository of definitions and proofs for real-time schedulability analysis. Its 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 on behalf of the readers is assumed.) To ensure full correctness, Prosa is written in and mechanically verified with Coq, a powerful and mature proof assistant with support for higher-order logic and computations.

See the Prosa paper for an in-depth introduction.

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.