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

van Chan Ngo (1) , Jean-Pierre Talpin (1) , Thierry Gautier (2)

1 ESPRESSO - Synchronous programming for the trusted component-based engineering of embedded systems and mission-critical systems
2 TEA - Tim, Events and Architectures

We present a method to construct a validator based on trans-lation validation approach to prove the value-equivalence of variables in 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). The validator proves that every output signal and its counterpart variable have the same val-ues by transforming the Sdvg graph.

Mots clés: Value-Graph; Graph Transformation; Formal Verification; Translation Validation; Certified Compiler; Synchronous Programs

Domaines: Systèmes embarqués

van Chan Ngo, Jean-Pierre Talpin, Thierry Gautier. Translation Validation for Synchronous Data-flow Specification in the SIGNAL Compiler. 2014. ⟨hal-01087801⟩