Formal Verification of Synchronous Data-flow Compilers

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