Skip to Main content Skip to Navigation
Journal articles

Compilation Modulaire d'un Langage Synchrone

Abstract : In this paper, we study the modular compilation of imperative synchronous programs. We rely on a formal framework well suited to perform compilation and formal validation of systems. In practice, we design and implement a special purpose language (LE) and its \execution equational semantics that allows the modular compilation of programs into software and hardware targets (C code, Vhdl code, FPGA synthesis, Verification tools). We show the correctness of this semantics, and we introduce a new algorithm to check program causality with respect to our modular approach. Relying in this formal approach, we defined a toolkit dedicated to the compilation and the verification of reactive applications.
Document type :
Journal articles
Complete list of metadata

Cited literature [24 references]  Display  Hide  Download
Contributor : Annie Ressouche Connect in order to contact the contributor
Submitted on : Friday, October 8, 2010 - 9:11:32 AM
Last modification on : Saturday, June 25, 2022 - 11:04:54 PM
Long-term archiving on: : Monday, January 10, 2011 - 11:38:30 AM


Files produced by the author(s)


  • HAL Id : inria-00524499, version 1



Annie Ressouche, Daniel Gaffé. Compilation Modulaire d'un Langage Synchrone. Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, Lavoisier, 2011, Application des méthodes formelles à l'analyse statique et la compilation, 4 (30), pp.441-471. ⟨inria-00524499⟩



Record views


Files downloads