Ph.D
Group :
Automotive embedded software design using formal methods
Starts on 07/10/2015
Advisor : BOULANGER, Frédéric
Funding :
Affiliation : Université Paris-Saclay
Laboratory : LRI
Defended on 09/12/2020, committee :
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
Research activities :
Abstract :
The growing share of driver assistance functions, their criticality, as well as the prospect of certification of these functions, make their verification and validation necessary with a level of requirement that testing alone cannot ensure.
For several years now, other industries such as aeronautics and railways have been subject to equivalent contexts. To respond to certain constraints, they have locally implemented formal methods. We are interested in the motivations and criteria that led to the use of formal methods in these industries in order to transpose them to automotive scenarios and identify the potential scope of application.
In this thesis, we present our case studies and propose methodologies for the use of formal methods by non-expert engineers. Inductive model checking for a model-driven development process, abstract interpretation to demonstrate the absence of run-time errors in the code and deductive proof for critical library functions.
Finally, we propose new algorithms to solve the problems identified during our experiments. These are, firstly, an invariant generator and a method using the semantics of data to process properties involving long-running timers in an efficient way, and secondly, an efficient algorithm to measure the coverage of the model by the properties using mutation techniques.
