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 metadatas

Cited literature [24 references]  Display  Hide  Download
Contributor : Annie Ressouche <>
Submitted on : Friday, October 8, 2010 - 9:11:32 AM
Last modification on : Tuesday, April 2, 2019 - 9:54:05 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 Théorie et Science Informatique, 2011, Application des méthodes formelles à l'analyse statique et la compilation, 4 (30), pp.441-471. ⟨inria-00524499⟩



Record views


Files downloads