Internships
Internship and research project proposals for ENAC 2nd-year students (2021). Contact pierre-loic.garoche@enac.fr for availability.
Comparaison de méthodes de partitionnement numérique en interprétation abstraite
On cherchera ici à expérimenter différentes méthodes de partitionnement de domaines abstraits pour la vérification de programmes numériques. Il s’agit de mettre au point différents exemples de code impératifs et de faire une évaluation de la précision de différentes méthodes de l’état de l’art.
Pré-requis: programmation OCaml
Continuous time components in CocoSim
Prise en compte des composants à temps continu dans CocoSim
L’objectif de ce stage est d’étendre CocoSim pour traiter les composants à temps continu. Pour l’instant, ils sont discrétisés et deviennent du code Lustre classique. Il s’agira de les compiler vers un langage à la Zélus.
En collaboration avec NASA Ames, nous développons CocoSim, une boîte à outils open-source pour Matlab Simulink, essentiellement motivée par les problématiques de vérification de modèles Simulink.
End to end verification of Lyapunov stability at code level
Vérification bout en bout de la stabilité d’un contrôleur au niveau du code
Il s’agit d’utiliser différents outils pour prouver automatiquement la stabilité d’un contrôleur à temps discret au niveau du code. L’idée sous-jacente est de pouvoir compiler les preuves comme on compile les modèles ou le code. Ainsi le modèle initial en Simulink est enrichi par un argument de stabilité (une fonction de Lyapunov), puis la preuve est compilée sous la forme d’une annotation de code Lustre, puis de code C.
Outils: CocoSim, LustreC, Frama-C, convex optimization solvers.
Design of a Neural Net based controller for a lander on Mars
Mise au point d’un contrôleur à base de réseau de neurones pour un atterrisseur Martien
Dans le cadre d’un projet avec l’ESA, nous étudions les propriétés d’algorithmes de guidage à base de réseau de neurones pour une mission d’atterrissage sur Mars. L’objectif de ce stage est d’expérimenter la conception d’un contrôleur NN par interpolation à partir d’un contrôleur de référence, pour la partie stabilisation et la partie guidage.
Stateflow automaton compilation
Compilation d’automates Stateflow
L’objectif de ce stage est d’étudier différentes méthodes de compilation des automates Stateflow dans CocoSim. CocoSim permet la vérification et la compilation de modèles Stateflow et Simulink en Lustre et en C.