Skip to Main content Skip to Navigation
New interface
Reports (Research report)

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 (Research report)
Complete list of metadata

Cited literature [22 references]  Display  Hide  Download
Contributor : Van Chan Ngo Connect in order to contact the contributor
Submitted on : Wednesday, January 30, 2013 - 1:47:11 PM
Last modification on : Wednesday, October 26, 2022 - 8:16:39 AM
Long-term archiving on: : Saturday, April 1, 2017 - 12:26:37 PM


Files produced by the author(s)


  • HAL Id : hal-00730926, version 5


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⟩



Record views


Files downloads