Composition du Jury:

- Björn Lisper, Rapporteur, Professor à l'Université de Mälardalen
- Andrew Tolmach, Rapporteur, Professor à Portland State University
- Xavier Leroy, Examinateur, Directeur de recherche à Inria Rocquencourt
- Marc Pantel, Examinateur, Maître de conférences à l'ENSEEIHT
- Christine Rochange, Examinatrice, Professeur des universités à l'Université de Toulouse III
- Sandrine Blazy, Directrice de thèse, Professeur des universités à l'Université de Rennes 1
- David Pichardie, Encadrant de thèse, Professeur des universités à l'ENS Rennes
- Isabelle Puaut, Co-Directrice de thèse, Professeur des universités à l'Université de Rennes 1

Résumé

Les systèmes informatiques critiques - tels que les commandes de vol électroniques et le contrôle des centrales nucléaires - doivent répondre à des exigences strictes en termes de sureté de fonctionnement.

Nous nous intéressons à l'application de méthodes formelles pour la vérification du comportement des logiciels critiques. Plus particulièrement, nous avons spécifié formellement des algorithmes et nous les avons prouvés corrects à l'aide de l'assistant à la preuve Coq, capable de vérifier mécaniquement la correction des preuves effectuées.

Nous avons travaillé sur la formalisation de l'estimation du Temps d'Exécution au Pire Cas (plus connu par son abréviation en anglais, WCET) de programmes C.
Le WCET est une propriété importante dans le développement des systèmes critiques, mais qui exige des analyses sophistiquées.
Pour garantir l'absence d'erreurs lors de ces analyses, nous avons formellement vérifié une méthode d'estimation du WCET fondée sur la combinaison de deux techniques principales: une estimation de bornes de boucles et une estimation du WCET via la méthode IPET (Implicit Path Enumeration Technique).
L'estimation de bornes de boucles est elle-même décomposée en trois étapes : un découpage de programmes, une analyse de valeurs opérant par interprétation abstraite, et une méthode de calcul de bornes.
Chacune de ces étapes est formellement vérifiée. Le développement a été intégré au compilateur C formellement vérifié CompCert.

Les contributions de cette thèse incluent la formalisation de techniques utilisées pour estimer le WCET, un outil d'estimation (obtenu à partir de la formalisation), et une évaluation expérimentale, incluant une comparaison avec des outils à l'état de l'art.