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.

Outils

CocoSim

Depuis quelques années, en collaboration avec NASA Ames, nous développons CocoSim, une boîte à outils open-source pour Matlab Simulink. Cette boîte à outils est essentiellement motivée par les problématiques de vérification de modèles Simulink mais est entièrement construite sur une architecture de compilateur.

Ainsi, grâce à CocoSim, on peut compiler un modèle Simulink discret en code C et utiliser ensuite ce code C pour effectuer des simulations ou pour l’exécuter sur le système embarqué.

Pour l’instant les composants continus sont discrétisés par Matlab.

• https://github.com/NASA-SW-VnV/CoCoSim

LustreC

LustreC est un compilateur écrit en Caml qui compile les modèles Lustre générés par CocoSim en code C. Il est capable de compiler les modèles Lustre qui contiennent des automates. Il n’est cependant pas capable de prendre en compte les modèles continus.

• https://cavale.enseeiht.fr/redmine/projects/lustrec

Zélus

Zélus est un langage synchrone capable d’exprimer les systèmes hybrides qui combinent temps discrets et modèles continus. Les programmes Zélus sont ensuite compilés pour être simulés de façon rigoureuse.

• https://zelus.di.ens.fr/

Travail à fournir / Tasks

• Enrichir CocoSim pour conserver les blocs continus sans les discrétiser
• Fournir un backend Zélus pour Cocosim, et/ou
• Enrichir LustreC pour y intégrer des constructions continues

Pré-requis / Requirements

• Connaissance de Matlab/Simulink
• Connaissance en langages synchrones
• Connaissance en contrôle (ODE)