Translation Validation for Transformations on Abstract Clocks in Synchronous Languages

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é : Validation de la traduction a été présenté comme une technique permettant de vérifier formellement l'exactitude des générateurs de code qui tente de vérifier que les transformations de programmes préservent la sémantique. Dans ce travail, nous adoptons cette approche de vérifier formellement que la sémantique d'horloge sont conservés pendant les transformations d'un compilateur de flux de données synchrone. Nous représentons la sémantique d'horloge d'un programme et son homologue transformé les formules du premier ordre qui sont appelés modèles d'horloge. Ensuite, nous introduisons une relation de raffinement qui exprime la préservation de la sémantique de l'horloge, comme un rapport sur ​​les modèles d'horloge. Notre validateur ne nécessite aucune instrumentation ou la modification du compilateur, ni aucune réécriture du programme source.
Type de document :
Rapport
[Research Report] RR-8064, INRIA. 2012
Liste complète des métadonnées


https://hal.inria.fr/hal-00730926
Contributeur : Van Chan Ngo <>
Soumis le : mercredi 30 janvier 2013 - 13:47:11
Dernière modification le : vendredi 13 janvier 2017 - 14:16:36
Document(s) archivé(s) le : samedi 1 avril 2017 - 12:26:37

Fichier

RR_8064.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00730926, version 5

Citation

Van Chan Ngo, Jean-Pierre Talpin, Thierry Gautier, Paul Le Guernic. Translation Validation for Transformations on Abstract Clocks in Synchronous Languages. [Research Report] RR-8064, INRIA. 2012. <hal-00730926v5>

Partager

Métriques

Consultations de
la notice

371

Téléchargements du document

119