Formal verification of automatically generated C-code from polychronous data-flow 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 : Synchronous data-flow languages are used as design approaches in developing embedded and critical real-time systems in which synchronous programs are verified by applying formal verification. In a synchronous design approach, transformation and optimization are used to transform synchronous programs and generate general purpose executable code. The incorrectness of the transformations make the guarantees unable to carry over the transformed programs and the executable code. In this work, adopting the translation validation approach, we present an automated verification process to verify the correctness of the synchronous language compiler Signal transformations and code generation on the clock information.
Type de document :
Communication dans un congrès
Accepted at HLDVT 2012, Nov 2012, California, United States. 2012
Liste complète des métadonnées

Littérature citée [23 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-00763781
Contributeur : Van Chan Ngo <>
Soumis le : mercredi 12 décembre 2012 - 11:07:54
Dernière modification le : vendredi 16 novembre 2018 - 01:23:15
Document(s) archivé(s) le : dimanche 18 décembre 2016 - 00:08:58

Fichier

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

Identifiants

  • HAL Id : hal-00763781, version 1

Collections

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

Citation

Van Chan Ngo, Loic Besnard, Thierry Gautier, Paul Le Guernic, Jean-Pierre Talpin. Formal verification of automatically generated C-code from polychronous data-flow equations. Accepted at HLDVT 2012, Nov 2012, California, United States. 2012. 〈hal-00763781〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

376

Téléchargements de fichiers

110

Contact


archive-ouverte@inria.fr