Lors de la cérémonie de remise du prix de thèse 2020, le Groupe De Recherche en Génie de la Programmation et du Logiciel (GDR-GPL) a remis le second prix à Valentin BESNARD pour sa thèse intitulée « EMI: Une approche pour unifier l’analyse et l’exécution embarquée à l’aide d’un interpréteur de modèles pilotable ».
Valentin a réalisé sa thèse sous la direction de Philippe DHAUSSY, Matthias BRUN, Ciprian TEODOROV et avec les conseils avisés de Frédéric JOUAULT et David OLIVIER. Cette distinction est le fruit de plus de trois ans de travail menés en collaboration avec l’ESEO, l’ENSTA Bretagne et Davidson Consulting.
Dans sa thèse, Valentin propose une approche novatrice permettant de concevoir et d’analyser des systèmes logiciels dans le but de garantir la sûreté de fonctionnement de ses systèmes et de détecter des erreurs de conception au plus tôt.
Cette approche se place idéalement dans le contexte actuel où les systèmes logiciels sont de plus en plus complexes et davantage exposés aux vulnérabilités.
Découvrez la thèse de Valentin BESNARD en visionnant la soutenance :
Pour comprendre plus en détail les travaux de recherche réalisés dans cette thèse, il faut tout d’abord s’intéresser aux techniques typiquement mises en œuvre pour concevoir un logiciel.
Les ingénieurs conçoivent tout d’abord un modèle dans un Langage de Modélisation (LM) permettant de décrire la structure et le comportement de ce système logiciel. Pour exécuter et analyser ce modèle, deux transformations sont généralement nécessaires.
- La première transforme le modèle de conception en un modèle d’analyse (décrit dans un Langage d’Analyse (LA) comme Fiacre ou Promela) sur lequel des techniques de vérification formelle (par exemple de model-checking) peuvent être appliquées.
- Le seconde transforme le modèle de conception en code exécutable (décrit dans un Langage d’Exécution (LE) comme le langage C ou l’assembleur) pouvant être déployé sur une plateforme d’exécution (par exemple une cible embarquée).
Cette approche de l’état de l’art fait apparaître trois grands problèmes:
- un fossé sémantique entre le modèle de conception et le modèle d’analyse qui rend plus complexe l’interprétation des résultats d’analyse par les ingénieurs de modélisation,
- un fossé sémantique entre le modèle de conception et le code exécutable qui rend plus complexe l’établissement de liens entre les concepts de modélisation et les portions de code exécutable,
- un problème d’équivalence entre le modèle d’analyse et le code exécutable qui ne permet pas de garantir que ce qui est exécuté est réellement ce qui a été vérifié en phase d’analyse.
Pour répondre à ces différentes problématiques, Valentin propose dans sa thèse une approche basée sur un interpréteur de modèle pilotable capturant une unique définition de la sémantique du langage.
Ainsi, le même modèle de conception et la même définition de la sémantique sont utilisés à la fois pour les activités d’analyse (par exemple simulation, débogage, model-checking) et l’exécution du système en production.
