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

https://hal.inria.fr/inria-00524499
Contributor : Annie Ressouche Connect in order to contact the contributor
Submitted on : Friday, October 8, 2010 - 9:11:32 AM
Last modification on : Thursday, February 11, 2021 - 2:56:34 PM
Long-term archiving on: : Monday, January 10, 2011 - 11:38:30 AM

File

RessoucheGaffe_TSI_24-03-2010....
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00524499, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

473

Files downloads

311