Translation Validation for Transformations on Abstract Clocks in Synchronous Languages

Van Chan Ngo 1 Jean-Pierre Talpin 1 Thierry Gautier 1 Paul Le Guernic 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 as a technique to formally verify the correctness of code generators that attempts to verify that program transformations preserve the semantics. In this work, we adopt this approach to formally verify that the clock semantics is preserved during the transformations of a synchronous data-flow compiler. We represent the clock semantics of a program and its transformed counterpart as first-order formulas which are called clock models. Then we introduce a refinement relation which expresses 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.
Document type :
Reports
Liste complète des métadonnées

Cited literature [22 references]  Display  Hide  Download

https://hal.inria.fr/hal-00730926
Contributor : Van Chan Ngo <>
Submitted on : Wednesday, January 30, 2013 - 1:47:11 PM
Last modification on : Friday, November 16, 2018 - 1:21:55 AM
Document(s) archivé(s) le : Saturday, April 1, 2017 - 12:26:37 PM

File

RR_8064.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00730926, version 5

Citation

Van Chan Ngo, Jean-Pierre Talpin, Thierry Gautier, Paul Le Guernic. Translation Validation for Transformations on Abstract Clocks in Synchronous Languages. [Research Report] RR-8064, INRIA. 2012. 〈hal-00730926v5〉

Share

Metrics

Record views

589

Files downloads

148