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.
Type de document :
Communication dans un congrès
International Conference on Formal Techniques for Distributed Objects, Components and Systems, Jun 2015, Grenoble, France. Springer, 9039, pp.66-80, Formal Techniques for Distributed Objects, Components, and Systems. 〈http://discotec2015.inria.fr〉. 〈10.1007/978-3-319-19195-9_5〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01148901
Contributeur : Jean-Pierre Talpin <>
Soumis le : mardi 5 mai 2015 - 16:16:11
Dernière modification le : mardi 16 janvier 2018 - 15:54:23

Identifiants

Citation

Van Chan Ngo, Jean-Pierre Talpin, Thierry Gautier. Translation Validation for Synchronous Data-flow Specification in the SIGNAL Compiler. International Conference on Formal Techniques for Distributed Objects, Components and Systems, Jun 2015, Grenoble, France. Springer, 9039, pp.66-80, Formal Techniques for Distributed Objects, Components, and Systems. 〈http://discotec2015.inria.fr〉. 〈10.1007/978-3-319-19195-9_5〉. 〈hal-01148901〉

Partager

Métriques

Consultations de la notice

225