Formal Verification of Synchronous Data-flow Compilers

Van Chan Ngo 1 Jean-Pierre Talpin 1 Thierry Gautier 1 Paul Le Guernic 1 Loic Besnard 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 : Synchronous data-flow languages have been used successfully for design and implementation of embedded and critical real-time systems. Synchronous language compilers compile programs to generate the executable code on particular platforms. To fulfill the high requirements of an efficient and reliable implementation, the correctness of the compilers must be guaranteed. This report aims at constructing a fully automated formal verification process to prove the correctness of a compiler for abstract clocks and clock relations (temporal constraints). We represent the source program and its compiled form (e.g. intermediate form, generated executable code) with polynomial dynamical systems and prove that the compiled form preserves the abstract clocks, and clock relations of the source program. In order to carry out this correctness proof, an appropriate relation called refinement and an automated proof method are provided. In this paper, the highly optimizing, industrial compiler from the widely used synchronous language SIGNAL to C is addressed.
Type de document :
Rapport
[Research Report] RR-7921, INRIA. 2012
Liste complète des métadonnées


https://hal.inria.fr/hal-00685633
Contributeur : Van Chan Ngo <>
Soumis le : mardi 17 avril 2012 - 16:10:13
Dernière modification le : vendredi 13 janvier 2017 - 14:16:43
Document(s) archivé(s) le : mercredi 14 décembre 2016 - 22:53:50

Fichier

RR-7921.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00685633, version 2

Citation

Van Chan Ngo, Jean-Pierre Talpin, Thierry Gautier, Paul Le Guernic, Loic Besnard. Formal Verification of Synchronous Data-flow Compilers. [Research Report] RR-7921, INRIA. 2012. <hal-00685633v2>

Partager

Métriques

Consultations de
la notice

358

Téléchargements du document

108