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.

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é.

CocoSim est capable de traiter certains modèles Stateflow également.

• 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.

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

Travail à fournir / Tasks

• Prise en main de l’outil CocoSim et des phases de compilation existantes des modèles Stateflow
• Proposition de plusieurs schémas de compilation
  • version implémentée
  • propositions de l’article Automated analysis of Stateflow models https://doi.org/10.29007/b8gq
• Mise en oeuvre manuelle puis automatisation.
• Comparaison de différents choix de modélisation (équivalence sémantique, efficacité de l’encodage en nombre d’opérations)
• Intégration à CocoSim et LustreC

Pré-requis / Requirements

• Programmation en Ocaml
• Connaissance de Matlab/Simulink