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

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.

Dans ce travail, nous décrivons comment la préservation de la valeur d'équivalence de variables peut être prouvée sur la base de la translation validation de valeur-graphe synchrone. Il se concentre sur ce qui prouve que toutes les variables de sortie dans le programme d'origine et leurs correspondants dans le programme transformé, le code C généré, ont les mêmes valeurs. Le calcul de chaque variable de sortie et son correspondant est représentée par une représentation formelle, un valeur-graphe partagé. Ce graphique représente la façon déterministe le calcul de la sortie dans le programme d'origine et son équivalent dans le programme transformé, et les noeuds pour les variables communes ont été partagées dans le graphique. Étant donné un SDVG, soutenons que nous voulons montrer que les deux variables de sortie ont la même valeur. Nous avons simplement besoin de verifier qu'ils sont représentés par des graphiques qui sont enracinées dans le même noeud du graphe. Nous parvenons à faire le chèque en normalisant SDVGs par des règles de réécriture.

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

Domaines: Systèmes embarqués

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⟩