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.
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.
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.