There are three main ways to use Prosa: either read the specification online (recommended for novices and researchers with a casual interest), download and check a specific release, or clone the Prosa repository (recommended for development).
The recommended way to read Prosa is by looking at the specification with low-level proofs omitted:
For reference, the specification with proofs and the full Coq source code are made available here:
See the getting started guide for a brief intro to essential Coq syntax.
To independently verify the correctness of the proofs, the full development can be downloaded, compiled, and validated with the Coq proof checker. This process is intentionally very simple and does not require any prior Coq knowledge.
For a short tutorial on how to check the proofs in Prosa, please follow the ECRTS’16 artifact evaluation instructions.
To start a new proof development or to contribute patches, it’s best to work with the Prosa git repository, which is publicly available on the MPI-SWS GitLab server.
To clone the repository, use the following command.
git clone https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs.git
For a tutorial on how to compile Prosa, please follow the setup instructions.
We periodically provide stable releases, which may be found below. Note that these releases are primarily intended as stable snapshots for ease of reference (e.g., to refer to a specific proof in a paper). For new developments and general improvements, please base your work on the current version (as found in the git repository).
The current releases of Prosa are based on Coq 8.5. For a step-by-step guide on how to install Prosa and its dependencies, please check out the setup instructions.
Released on June 6th, 2016. Tested with Coq 8.5pl1 and ssreflect 1.6.
view specification (without proof scripts)
view specification (with proof scripts)
Prosa v0.2 incorporates the reduction-based response-time analysis (RTA) for real-time scheduling with arbitrary processor affinities (APA). See the overview page for more information.
Released on May 5th, 2016. Tested with Coq 8.5pl1 and ssreflect 1.6.
Prosa v0.1 formalizes Bertogna and Cirinei’s response-time analysis (RTA) for global FP and EDF scheduling, along with extensions for release jitter and parallel jobs. For additional information, please follow the ECRTS’16 artifact evaluation instructions.