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
Résumé : 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.
Type de document :
Rapport
[Research Report] RR-8508, INRIA. 2014, pp.43
Liste complète des métadonnées


https://hal.inria.fr/hal-00962430
Contributeur : Van Chan Ngo <>
Soumis le : vendredi 28 mars 2014 - 10:23:32
Dernière modification le : vendredi 13 janvier 2017 - 14:17:56
Document(s) archivé(s) le : samedi 28 juin 2014 - 11:06:57

Fichier

RR-8508.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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>

Partager

Métriques

Consultations de
la notice

362

Téléchargements du document

131