Vendredi 18 Décembre 2020
- Share
- Share on Facebook
- Share on X
- Share on LinkedIn
Outils Certifiés pour les Analyses d'Ordonnançabilité
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.
Date et Lieu
Vendredi 18 Décembre à 10:00
https://grenoble-inp.zoom.us/j/96952134330
Organisé par
Xiaojie GUO
Composition du Jury
INRIA Grenoble, Directeur de thèse
University of York, Rapporteur
INRIA Nancy, Rapporteur
University of Luxembourg, Examinateur
CNRS, Examinateur
Université Grenoble Alpes, Invité (Co-directeur de thèse)
INRIA Grenoble, Invitée (Co-encadrante)
- Share
- Share on Facebook
- Share on X
- Share on LinkedIn