Les spécifications basées sur les schémas-blocs et machines à états sont utilisées pour la conception de systèmes de contrôle-commande, particulièrement dans le développement d’applications critiques. Des outils tels que Scade et Simulink/Stateflow sont équipés de compilateurs qui traduisent de telles spécifications en code exécutable. Ils proposent des langages de programmation permettant de composer des fonctions sur des flots, tel que l’illustre le langage synchrone à flots de données Lustre.
Cet exposé présente Vélus, un compilateur Lustre vérifié dans l’assistant de preuves interactif Coq. Nous développons des modèles sémantiques pour les langages de la chaîne de compilation, et utilisons le compilateur C vérifié CompCert pour générer du code exécutable et donner une preuve de correction de bout en bout.
Le défi principal est de montrer la préservation de la sémantique entre le paradigme flots de données et le paradigme impératif, et de raisonner sur la représentation bas niveau de l’état d’un programme. En particulier, nous traitons le reset modulaire, une primitive pour réinitialiser des sous-systèmes. Ceci implique la mise en place de modèles sémantiques adéquats, d’algorithmes de compilation et des preuves de correction correspondantes.
Dans un second temps, une autre approche de la compilation vérifiée est présentée dans le cadre d'un travail de recherche actuel sur le compilateur LustreC. Ce travail consiste à transformer LustreC en compilateur certifiant, qui génère du code et de la spécification associée prouvée a posteriori par des outils comme Frama-C ou SPARK.
Vidéo disponible ici : https://prismes.univ-toulouse.fr/player.php?code=70Bn133d&width=100%&height=100%