Skip to Main content Skip to Navigation

Evaluating SDVG translation validation: from Signal to C

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 : In this work, we describe how the preservation of value-equivalence of variables can be proved based on translation validation of synchronous data-flow value-graphs. It focuses on proving that every output variables in the original program and their counterparts in the transformed program, the generated C code, have the same values. The computation of each output variable and its counterpart is represented by a formal representation, a shared value-graph. This graph deterministically represents the computation of the output in the original program and its counterpart in the transformed program, and the nodes for the common variables have been shared in the graph. Given a SDVG, support that we want to show that the two output variables have the same value. We simply need to check that they are represented by graphs which are rooted at the same graph node. We manage to make the check by normalizing SDVGs by some rewrite rules.
Document type :
Complete list of metadata

Cited literature [14 references]  Display  Hide  Download
Contributor : Van Chan Ngo Connect in order to contact the contributor
Submitted on : Friday, March 28, 2014 - 10:23:32 AM
Last modification on : Friday, February 4, 2022 - 3:12:50 AM
Long-term archiving on: : Saturday, June 28, 2014 - 11:06:57 AM


Files produced by the author(s)


  • HAL Id : hal-00962430, version 2


van Chan Ngo, Jean-Pierre Talpin, Thierry Gautier, Paul Le Guernic. Evaluating SDVG translation validation: from Signal to C. [Research Report] RR-8508, INRIA. 2014, pp.43. ⟨hal-00962430v2⟩



Record views


Files downloads