Formal verification of automatically generated C-code from polychronous data-flow equations - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2012

Formal verification of automatically generated C-code from polychronous data-flow equations

Résumé

Synchronous data-flow languages are used as design approaches in developing embedded and critical real-time systems in which synchronous programs are verified by applying formal verification. In a synchronous design approach, transformation and optimization are used to transform synchronous programs and generate general purpose executable code. The incorrectness of the transformations make the guarantees unable to carry over the transformed programs and the executable code. In this work, adopting the translation validation approach, we present an automated verification process to verify the correctness of the synchronous language compiler Signal transformations and code generation on the clock information.
Fichier principal
Vignette du fichier
report.pdf (325.84 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00763781 , version 1 (12-12-2012)

Identifiants

  • HAL Id : hal-00763781 , version 1

Citer

van Chan Ngo, Loic Besnard, Thierry Gautier, Paul Le Guernic, Jean-Pierre Talpin. Formal verification of automatically generated C-code from polychronous data-flow equations. HLDVT 2012 - IEEE International High-Level Design, Validation and Test Workshop, Nov 2012, California, United States. ⟨hal-00763781⟩
171 Consultations
89 Téléchargements

Partager

Gmail Facebook X LinkedIn More