Formal Verification of Synchronous Data-flow Compilers

Van Chan Ngo 1 Jean-Pierre Talpin 1 Thierry Gautier 1 Paul Le Guernic 1 Loic Besnard 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
Abstract : Synchronous data-flow languages have been used successfully for design and implementation of embedded and critical real-time systems. Synchronous language compilers compile programs to generate the executable code on particular platforms. To fulfill the high requirements of an efficient and reliable implementation, the correctness of the compilers must be guaranteed. This report aims at constructing a fully automated formal verification process to prove the correctness of a compiler for abstract clocks and clock relations (temporal constraints). We represent the source program and its compiled form (e.g. intermediate form, generated executable code) with polynomial dynamical systems and prove that the compiled form preserves the abstract clocks, and clock relations of the source program. In order to carry out this correctness proof, an appropriate relation called refinement and an automated proof method are provided. In this paper, the highly optimizing, industrial compiler from the widely used synchronous language SIGNAL to C is addressed.
Document type :
Reports
Liste complète des métadonnées

Cited literature [21 references]  Display  Hide  Download

https://hal.inria.fr/hal-00685633
Contributor : Van Chan Ngo <>
Submitted on : Tuesday, April 17, 2012 - 4:10:13 PM
Last modification on : Friday, November 16, 2018 - 1:23:42 AM
Document(s) archivé(s) le : Wednesday, December 14, 2016 - 10:53:50 PM

File

RR-7921.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00685633, version 2

Citation

Van Chan Ngo, Jean-Pierre Talpin, Thierry Gautier, Paul Le Guernic, Loic Besnard. Formal Verification of Synchronous Data-flow Compilers. [Research Report] RR-7921, INRIA. 2012. ⟨hal-00685633v2⟩

Share

Metrics

Record views

530

Files downloads

152