Formal proofs for the analysis of real-time systems in Coq

Schedulability analysis aims at guaranteeing the absence of deadline misses in hard real-time systems. This property is crucial for systems used in safety-critical domains such as avionics because a single deadline miss may have catastrophic consequences.

In this thesis, we use the Coq proof assistant and machine-checked proofs to provide the highest level of confidence in hard real-time system schedulability analyses as well as related industrial tools.

The main contributions of this thesis are:
(i) A formal interface combining the schedulability analyses proven in the Prosa library based on Coq with a formally verified OS kernel (RT-CertiKOS). This work demonstrated the adequacy of Prosa's abstract model with a real system and showed that analyses proven over an abstract and analysis-convenient models can also be applied to a concrete system. This work also provided RT-CertiKOS with a modular, state-of-the-art schedulability analysis proof.
(ii) CertiCAN, a formally verified result certifier for CAN (Controller Area Network) analyzers. This work showed that result certification is a flexible and light-weight process suitable for industry practice. Indeed, it does not rely on the source code and is not impacted by software updates. Our experiments show that CertiCAN is efficient enough to certify the results produced by the industrial tool RTaW-Pegase even for large systems.
(iii) Gd, a very general task model and its corresponding response time analysis amenable to a formalization in Coq. The main benefit of this approach is to factorize and reduce the proof effort. After verifying a general schedulability analysis for Gd, proving the correctness of analysis for a more specific model boils down to proving its instantiation to Gd.