Vérification de la génération modulaire du code impératif pour Lustre

Timothy Bourke 1, 2 Pierre-Evariste Dagand 3 Marc Pouzet 1, 2, 4 Lionel Rieg 5, 6
2 Parkas - Parallélisme de Kahn Synchrone
DI-ENS - Département d'informatique de l'École normale supérieure, ENS Paris - École normale supérieure - Paris, CNRS - Centre National de la Recherche Scientifique, Inria de Paris
3 Whisper - Well Honed Infrastructure Software for Programming Environments and Runtimes
LIP6 - Laboratoire d'Informatique de Paris 6, Inria de Paris
Résumé : Les langages synchrones sont utilisés pour programmer des logiciels de contrôle-commande d'applications critiques. Le langage Scade, utilisé dans l'industrie pour ces applications, est fondé sur le langage Lustre introduit par Caspi et Halbwachs. On s'intéresse ici à la formalisation et la preuve, dans l'assistant de preuve Coq, d'une étape clef de la compilation : la traduction de programmes Lustre vers des programmes d'un langage impératif. Le défi est de passer d'une sémantique synchrone flot de données, où un programme manipule des flots, à une sémantique impérative, où un programme manipule la mémoire de façon séquentielle. Nous spécifions et vérifions un générateur de code simple qui gère les traits principaux de Lustre : l'échantillonnage, les noeuds et les délais. La preuve utilise un modèle sémantique intermédiaire qui mélange des traits flot de données et impératifs et permet de définir un invariant inductif essentiel. Nous exploitons la formalisation proposée pour vérifier une optimisation classique qui fusionne des structures conditionnelles dans le code impératif généré.
Type de document :
Communication dans un congrès
JFLA 2017 - Vingt-huitième Journées Francophones des Langages Applicatifs, Jan 2017, Gourettes, France. <http://jfla.inria.fr/2017/index.html>
Liste complète des métadonnées

https://hal.inria.fr/hal-01403830
Contributeur : Timothy Bourke <>
Soumis le : lundi 28 novembre 2016 - 12:17:20
Dernière modification le : lundi 3 avril 2017 - 09:01:15
Document(s) archivé(s) le : mardi 21 mars 2017 - 00:42:11

Identifiants

  • HAL Id : hal-01403830, version 1

Collections

Citation

Timothy Bourke, Pierre-Evariste Dagand, Marc Pouzet, Lionel Rieg. Vérification de la génération modulaire du code impératif pour Lustre. JFLA 2017 - Vingt-huitième Journées Francophones des Langages Applicatifs, Jan 2017, Gourettes, France. <http://jfla.inria.fr/2017/index.html>. <hal-01403830>

Partager

Métriques

Consultations de
la notice

258

Téléchargements du document

270