Description
Date depot: 4 juillet 2022
Titre: Langage de programmation réactif appliqué à la spécification fonctionnelle automobile et la conception par modélisation
Directrice de thèse:
Christine TASSON (ISAE-SUPAERO)
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Programmation et architecture logicielle
Resumé: Le but de la thèse est le prototypage d'un langage de spécification fonctionelle adapté à l'industrie
automobile et de prouver l'efficacité de la programmation fonctionnelle réactive (FRP) dans la
conception par modélisation de logiciels sûrs et efficaces .
Une première étape consistera à analyser les exigences de construction liées au cadre d'application
de l'industrie automobile et résultera en une syntaxe et une sémantique du langage prototypé,
facilement manipulable et compréhensible. Les programmes seront alors traduits vers une
représentation intermédiaire adaptée à l'analyse du niveau de sûreté des programmes selon le
standard ISO-26262 via des outils formels comme la vérification et l'analyse statique.
Une deuxième étape sera dédiée à la conception du transpileur – générateur de code – vers un langage
de programmation industriel. En s'appuyant sur des cas concrets (comme par exemple la conception
d'un contrôleur de fusion pour la détection des piétons et cyclistes), le code généré sera intégré dans
un environnement de simulation de type Modelica, afin d'établir la pertinence du langage par la
vérification fonctionnelle du code en mode Software in the loop (SIL), ainsi que la vérification des
performances en mode Hardware in the loop (PIL/HIL).
Finalement, en supposant que le compilateur du langage cible est correct, on s'attachera à certifier
l'absence d'erreur du transpileur : le programme initial et son code généré sont observationnellement
équivalent (ils ont le même comportement dans n'importe quel environnement d'exécution). On
s'appuiera notamment sur des assistants de preuve tels que Coq et Why3 et sur les méthodes de
vérification formelle du code généré.
Doctorant.e: Thome Emilie