Formal Verification of Compiler Transformations on Polychronous Equations

Van Chan Ngo 1 Loic Besnard 1 Thierry Gautier 1 Paul Le Guernic 1 Jean-Pierre Talpin 1
1 ESPRESSO - Synchronous programming for the trusted component-based engineering of embedded systems and mission-critical systems
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : In this paper, adopting the translation validation approach, we present a formal verification process to prove the correctness of compiler transformations on systems of polychronous equations. We encode the source programs and the transformations with polynomial dynamical systems and prove that the transformations preserve the abstract clocks and clock relations of the source programs. In order to carry out the correctness proof, an appropriate relation called refinement and an automated proof method are presented. Each individual transformation or optimization step of the compiler is followed by our validation process which proves the correctness of this running. The compiler will continue its work if and only if the correctness is proved positively. In this paper, the highly optimizing, industrial compiler from the synchronous language SIGNAL to C is addressed.
Type de document :
Communication dans un congrès
International Conference on Integrated Formal Methods, Jun 2012, Pisa, Italy. 2012
Liste complète des métadonnées

Littérature citée [16 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-00730393
Contributeur : Van Chan Ngo <>
Soumis le : lundi 10 septembre 2012 - 10:21:19
Dernière modification le : mercredi 11 avril 2018 - 02:01:14
Document(s) archivé(s) le : mardi 11 décembre 2012 - 03:39:04

Fichier

ifm12.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00730393, version 1

Collections

INRIA | IRISA | IRISA-D4 | UR1-UFR-ISTIC | UNIV-RENNES | INRIA-RENGRE

Citation

Van Chan Ngo, Loic Besnard, Thierry Gautier, Paul Le Guernic, Jean-Pierre Talpin. Formal Verification of Compiler Transformations on Polychronous Equations. International Conference on Integrated Formal Methods, Jun 2012, Pisa, Italy. 2012. 〈hal-00730393〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

406

Téléchargements de fichiers

116

Contact


archive-ouverte@inria.fr