RT-proofs

RT-Proofs project is an international research collaboration between TU Braunschweig, INRIA, MPI-SWS, Onera, and Verimag. It is funded by ANR and DFG for the period of 3 years (from January 2018 until December 2020).

The currently used analysis methods in the area of real-time systems are often based on informal proofs, which are difficult to follow, check or reuse, and hence at risk of subtle but fatal mistakes. As a result, an alarming number of unsound results had to be corrected in recent years. RT-proofs project is motivated by these facts, and its objective is to lay the foundations for the computer-assisted verification of schedulability analysis methods and proofs. To that aim, the following activities will be performed:

• A uniform, consistent, and precise formalisation of core concepts of the real-time scheduling theory will be developed.
• A set of essential foundational analysis techniques used in the real-time domain will be formalised and certified in the Coq proof assistant.
• Possibilities to certify results provided by commercial analysis tools (e.g. SymTA/S, NETCAR-Analyzer, RTaW Pegase) will be investigated.

TU Braunschweig participates in all the aforementioned activities, and is the leader of the first activity.