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, CNRS - Centre National de la Recherche Scientifique, Inria de Paris
3 Whisper - Well Honed Infrastructure Software for Programming Environments and Runtimes
Inria de Paris, LIP6 - Laboratoire d'Informatique de Paris 6
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é.
Complete list of metadatas

Cited literature [22 references]  Display  Hide  Download

https://hal.inria.fr/hal-01403830
Contributor : Timothy Bourke <>
Submitted on : Monday, November 28, 2016 - 12:17:20 PM
Last modification on : Thursday, March 21, 2019 - 2:17:10 PM
Long-term archiving on : Tuesday, March 21, 2017 - 12:42:11 AM

Identifiers

  • HAL Id : hal-01403830, version 1

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, Gourette, France. ⟨hal-01403830⟩

Share

Metrics

Record views

580

Files downloads

845