A Foundation for Formally Proven Schedulability Analysis

What is Prosa?

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.

Why should I use Prosa?

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:

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

  (* Assume that jobs are sequential. *)
  Hypothesis H_sequential_jobs: sequential_jobs sched.

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.

  (* Let j be any job in the arrival sequence. *)
  Variable j: JobIn arr_seq.

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

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

Where can I learn more?

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.