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

L'analyse d'ordonnançabilité vise à garantir le respect des échéances dans les systèmes temps réel durs. Cette propriété est cruciale pour les systèmes utilisés dans les domaines critiques tels que l'avionique, car une échéance manquée peut avoir des conséquences catastrophiques. Dans cette thèse, nous utilisons l'assistant de preuves Coq afin d'assurer la correction des analyses d'ordonnançabilité des systèmes temps réel durs et des outils industriels associés.

Les principales contributions de cette thèse sont:
(i) Une interface formelle combinant les analyses d'ordonnançabilité prouvées dans la bibliothèque Prosa basée sur Coq avec un noyau de système d'exploitation concret vérifié formellement (RT-CertiKOS). Ce travail a permis de justifier l'adéquation du modèle abstrait de Prosa à un système réel. Il a montré que les analyses prouvées pour un modèle abstrait et dédié à l'analyse peuvent également être appliquées à un système concret. Ce travail a également fourni à RT-CertiKOS une preuve d'ordonnançabilité modulaire à la pointe de l'état de l'art.
(ii) CertiCAN, un certificateur de résultats formellement vérifié pour les analyseurs de réseaux CAN (Controller Area Network). Ce travail a montré que la certification de résultats est un processus flexible et léger qui convient bien aux pratiques de l'industrie. En effet, CertiCAN n'a pas besoin d'avoir accès au code source et n'est pas affecté par les mises à jour logicielles. Nos expérimentations ont montré que CertiCAN est suffisamment efficace pour certifier les résultats produits par l'outil industriel RTaW-Pegase et ceci même pour de grands systèmes.
(iii) Gd, un modèle de tâches très général et une  analyse du temps de réponse associée se prêtant à sa formalisation en Coq. L'avantage de cette approche est de factoriser et de simplifier l'effort de preuve. Une fois l'analyse du temps de réponse pour Gd formellement vérifiée, prouver la correction d'une analyse pour un modèle plus spécifique revient à prouver son instanciation à Gd.