Doctorat
Equipe :
Intégration de méthodes formelles dans la conception des fonctions logicielles automobiles
Début le 07/10/2015
Direction : BOULANGER, Frédéric
Ecole doctorale : ED STIC 580
Etablissement d'inscription : Université Paris-Saclay
Lieu de déroulement : LRI
Soutenue le 09/12/2020 devant le jury composé de :
Rapporteurs et examinateurs :
- Gérard Berry, Professeur, Collège de France
- Cesare Tinelli, Professeur, University of Iowa
Examinateurs :
- Sylvie Putot, Professeur, Ecole Polytechnique
- Pascale Le Gall, Professeur, CentraleSupélec
- Fabrice Kordon, Professeur, Sorbonne Université
- Sylvain Conchon, Professeur, Université Paris-Saclay
Directeur de thèse :
- Frédéric Boulanger, Professeur, CentraleSupélec
Co-encadrant de thèse :
- Safouan Taha, Maître de conférences, CentraleSupélec
Tuteur industriel :
- Armando Hernandez, Maître-expert logiciel, Groupe PSA
Activités de recherche :
Résumé :
La part croissante des fonctions d'assistance à la conduite, leur criticité, ainsi que la perspective d'une certification de ces fonctions, rendent nécessaire leur vérification et leur validation avec un niveau d'exigence que le test seul ne peut assurer.
Depuis quelques années déjà d’autres domaines comme l’aéronautique ou le ferroviaire sont soumis à des contextes équivalents. Pour répondre à certaines contraintes ils ont localement mis en place des méthodes formelles. Nous nous intéressons aux motivations et aux critères qui ont conduit à l’utilisation des méthodes formelles dans ces domaines afin de les transposer sur des scénarios automobiles et identifier le périmètre potentiel d'application.
Dans cette thèse, nous présentons nos études de cas et proposons des méthodologies pour l'usage de méthodes formelles par des ingénieurs non-experts. Le model checking inductif pour un processus de développement utilisant des modèles, l'interprétation abstraite pour démontrer l'absence d'erreurs d'exécution du code et la preuve déductive pour des cas de fonctions critiques de librairie.
Enfin, nous proposons de nouveaux algorithmes pour résoudre les problèmes identifiés lors de nos expérimentations. Il s'agit d'une part d'un générateur d'invariants et d'une méthode utilisant la sémantique des données pour traiter efficacement des propriétés comportant du temps long, et d'autre part d'un algorithme efficace pour mesurer la couverture du modèle par les propriétés en utilisant des techniques de mutation.
