Formal Verification of Synchronous Data-flow Program Transformations Toward Certified Compilers

Van Chan Ngo 1 Loïc Besnard 1 Paul Le Guernic 1 Jean-Pierre Talpin 1 Thierry Gautier 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 : Translation validation was introduced in the 90's by Pnueli et al. as a technique to formally verify the correctness of code generators. Rather than certifying the code generator or exhaustively qualifying it, translation validators attempt to verify that program transformations preserve semantics. In this work, we adopt this approach to formally verify that the clock semantics and data dependence are preserved during the compilation of the Signal compiler. Translation validation is implemented for every compilation phase from the initial phase until the latest phase where the executable code is generated, by proving that the transformation in each phase of the compiler preserves the semantics. We represent the clock semantics, the data dependence of a program and its transformed counterpart as first-order formulas which are called Clock Models and Synchronous Dependence Graphs (SDGs), respectively. Then we introduce clock refinement and dependence refinement relations which express the preservation of clock semantics and dependence, as a relation on clock models and SDGs, respectively. Our validator does not require any instrumentation or modification of the compiler, nor any rewriting of the source program.
Type de document :
Article dans une revue
Frontiers of Computer Science, Springer Verlag, 2013
Liste complète des métadonnées

Littérature citée [34 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00846279
Contributeur : Van Chan Ngo <>
Soumis le : jeudi 18 juillet 2013 - 17:50:57
Dernière modification le : mercredi 16 mai 2018 - 11:23:02
Document(s) archivé(s) le : mercredi 5 avril 2017 - 14:58:04

Fichier

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

Identifiants

  • HAL Id : hal-00846279, version 1

Citation

Van Chan Ngo, Loïc Besnard, Paul Le Guernic, Jean-Pierre Talpin, Thierry Gautier. Formal Verification of Synchronous Data-flow Program Transformations Toward Certified Compilers. Frontiers of Computer Science, Springer Verlag, 2013. 〈hal-00846279〉

Partager

Métriques

Consultations de la notice

733

Téléchargements de fichiers

211