Il s'agit d'utiliser différents outils pour prouver automatique 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. La preuve de stabilité est ensuite compilée sous la forme d'une annotation de code Lustre, puis de code C. L'objectif de ce stage est d'automatiser le processus.
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 ici de les compiler vers un langage à la Zelus.
[Stage pourvu.] L'objectif de ce stage est d'étudier différentes méthodes ou schémas de compilation des automates dans CocoSim. CocoSim est un outil NASA intégré à Simulink qui permet la vérification et la compilation de modèle Stateflow et Simulink en lustre et en C.
[Stage pourvu.] Conception d'un réseau de neurone /contrôleur/ par interpolation à partir d'un contrôleur de référence, tant pour la partie stabilisation que pour la partie guidage.
[Stage pourvu.] On cherchera ici à expérimenter différentes méthodes de partitionnement de domaines abstraits pour la vérification de programmes numériques.