At the 2020 thesis award ceremony, the Groupe De Recherche en Génie de la Programmation et du Logiciel (GDR-GPL) awarded second prize to Valentin BESNARD for his thesis entitled “EMI: Une approche pour unifier l’analyse et l’exécution embarquée à l’aide d’un interpréteur de modèles pilotable”.
Valentin completed his thesis under the supervision of Philippe DHAUSSY, Matthias BRUN, Ciprian TEODOROV and with the expert advice of Frédéric JOUAULT and David OLIVIER. This award is the fruit of more than three years’ work in collaboration withESEO,ENSTA Bretagne and Davidson Consulting.
In his thesis, Valentin proposes an innovative approach to the design and analysis of software systems, with the aim of guaranteeing the dependability of these systems and detecting design errors at an early stage.
This approach is ideally suited to the current context in which software systems are becoming increasingly complex and more exposed to vulnerabilities.
Find out more about Valentin BESNARD’s thesis by watching his defence:
To understand the research work carried out in this thesis in more detail, we first need to look at the techniques typically used to design software.
Engineers first design a model in a Modelling Language (ML) to describe the structure and behaviour of the software system. To execute and analyse this model, two transformations are generally necessary.
- The first transforms the design model into an analysis model (described in an Analysis Language (AL) such as Fiacre or Promela) on which formal verification techniques (e.g. model-checking) can be applied.
- The second transforms the design model into executable code (described in an Execution Language (EL) such as C or assembler) that can be deployed on an execution platform (e.g. an embedded target).
This state-of-the-art approach highlights three main problems:
- a semantic gap between the design model and the analysis model, which makes it more complex for modelling engineers to interpret analysis results,
- a semantic gap between the design model and the executable code, which makes it more complex to establish links between modelling concepts and portions of executable code,
- a problem of equivalence between the analysis model and the executable code, which makes it impossible to guarantee that what is executed is actually what was verified during the analysis phase.
To address these issues, Valentin’s thesis proposes an approach based on a controllable model interpreter that captures a single definition of the language’s semantics.
In this way, the same design model and the same definition of semantics are used for both analysis activities (e.g. simulation, debugging, model-checking) and system execution in production.
