Translation Validation for Clock Transformations in a Synchronous Compiler

Van Chan Ngo 1, 2 Jean-Pierre Talpin 2 Thierry Gautier 2 Paul Le Guernic 2
1 ESTASYS - Efficient STAtistical methods in SYstems of systems
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
2 TEA - Tim, Events and Architectures
IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL, Inria Rennes – Bretagne Atlantique
Abstract : Translation validation was introduced as a technique to for-mally verify the correctness of code generators that attempts to verify that program transformations preserve the semantics. In this work, we adopt this approach to construct a validator that formally verifies the preservation of clock semantics during the Signal compiler transforma-tions. The clock semantics is represented as a first-order logic formula called clock model. Then we introduce a refinement relation which ex-presses the preservation of clock semantics, as a relation on clock models. Our validator does not require any instrumentation or modification of the compiler, nor any rewriting of the source program.
Type de document :
Communication dans un congrès
FASE - ETAPS 2015, Apr 2015, London, United Kingdom. Springer, 2015
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01087795
Contributeur : Van Chan Ngo <>
Soumis le : vendredi 17 avril 2015 - 11:12:27
Dernière modification le : mardi 16 janvier 2018 - 15:54:23
Document(s) archivé(s) le : mardi 18 avril 2017 - 22:45:36

Identifiants

  • HAL Id : hal-01087795, version 3

Citation

Van Chan Ngo, Jean-Pierre Talpin, Thierry Gautier, Paul Le Guernic. Translation Validation for Clock Transformations in a Synchronous Compiler. FASE - ETAPS 2015, Apr 2015, London, United Kingdom. Springer, 2015. 〈hal-01087795v3〉

Partager

Métriques

Consultations de la notice

351

Téléchargements de fichiers

117