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 :
Reports
Liste complète des métadonnées

Cited literature [14 references]  Display  Hide  Download

https://hal.inria.fr/hal-00962430
Contributor : Van Chan Ngo <>
Submitted on : Friday, March 28, 2014 - 10:23:32 AM
Last modification on : Friday, November 16, 2018 - 1:23:23 AM
Document(s) archivé(s) le : Saturday, June 28, 2014 - 11:06:57 AM

File

RR-8508.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00962430, version 2

Citation

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⟩

Share

Metrics

Record views

508

Files downloads

162