Translation Validation for Synchronous Data-Flow Specification in the SIGNAL Compiler

Van Chan Ngo 1 Jean-Pierre Talpin 2 Thierry Gautier 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
IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL, Inria Rennes – Bretagne Atlantique
Abstract : We present a method to construct a validator based on translation validation approach to prove the value-equivalence of variables in the compilation of the Signal compiler. The computation of output signals in a Signal program and their counterparts in the generated C code is represented by a Synchronous Data-flow Value-Graph (Sdvg). Our validator proves that every output signal and its counterpart variable have the same values by transforming the Sdvg graph.
Complete list of metadatas

Cited literature [16 references]  Display  Hide  Download

https://hal.inria.fr/hal-01767328
Contributor : Hal Ifip <>
Submitted on : Monday, April 16, 2018 - 10:18:48 AM
Last modification on : Thursday, November 15, 2018 - 11:58:49 AM

File

978-3-319-19195-9_5_Chapter.pd...
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Van Chan Ngo, Jean-Pierre Talpin, Thierry Gautier. Translation Validation for Synchronous Data-Flow Specification in the SIGNAL Compiler. 35th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2015, Grenoble, France. pp.66-80, ⟨10.1007/978-3-319-19195-9_5 ⟩. ⟨hal-01767328⟩

Share

Metrics

Record views

384

Files downloads

146