Skip to Main content Skip to Navigation
Conference papers

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
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
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.
Complete list of metadata

Cited literature [22 references]  Display  Hide  Download

https://hal.inria.fr/hal-01087795
Contributor : van Chan Ngo <>
Submitted on : Friday, April 17, 2015 - 11:12:27 AM
Last modification on : Friday, January 8, 2021 - 3:40:37 AM
Long-term archiving on: : Tuesday, April 18, 2017 - 10:45:36 PM

Files

Identifiers

  • 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. ⟨hal-01087795v3⟩

Share

Metrics

Record views

546

Files downloads

388