The overall objective of the RT- PROOFS project is to lay the foundations for computer-assisted formal verification of timing analysis results. More precisely, we will provide:
- a strong formal basis for schedulability, blocking, and response-time analysis supported by the
Coq proof assistant, that is as generic, robust, and modular as possible; - correctness proofs for well-established as well as new, generalized response-time analysis results, and a better, precise understanding of the role played by key assumptions and formal connections between competing analysis techniques;
- an approach for the generation of proof certificates so that analysis results — in contrast to analysis tools — can be certified.
The first objective will allow us to base all further proofs on a formal basis that is sufficiently generic to be understood and accepted by all members of the real-time community. This is crucial because many researchers use different models for their analyses, sometimes making implicit assumptions (e.g., absence of scheduling overhead, discrete versus dense time, etc.), which renders the comparison and compositions of results difficult and therefore in general informal only.
The second objective will force us to make all assumptions explicit, to understand better where exactly they are needed, and whether they can be weakened. By doing so, we will also establish if and how common analysis techniques are in fact compatible (i.e., based on similar assumptions), and how popular analysis techniques may be adapted to lift restrictive assumptions, e.g., related to suspension times.
The third objective is to clearly demonstrate with a convincing proof of concept that result certification for response-time analysis tools is feasible.
