Skip to Main content Skip to Navigation
Journal articles

ESTEREL: A formal method applied to avionic software development

Gérard Berry 1 Amar Bouali 2 Xavier Fornari 1 Emmanuel Ledinot 3 Eric Nassor 3 Robert de Simone 2 
2 TICK - Theory and Practice of Synchronous Reactive Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , MINES ParisTech - École nationale supérieure des mines de Paris
Abstract : Dassault Aviation is a French aircraft manufacturer building civil business jets (the Falcon family) and military jet fighters (the Mirage and Rafale families). It has been concerned with formal methods inside the development process of avionic software since 1989. In this paper, we give a comprehensive account of three industrial-size studies carried out at Dassault Aviation using the reactive synchronous language ESTEREL and its toolset, in collaboration with the public research team that develops ESTEREL at Ecole des Mines de Paris and INRIA Sophia-Antipolis. We deal with software engineering issues related to compilation, optimization and verification of safety-critical embedded software. The goal is to ensure production of efficient and reliable code.
Document type :
Journal articles
Complete list of metadata
Contributor : Magalie Prudon Connect in order to contact the contributor
Submitted on : Thursday, March 24, 2011 - 2:34:16 PM
Last modification on : Friday, February 4, 2022 - 3:20:09 AM

Links full text



Gérard Berry, Amar Bouali, Xavier Fornari, Emmanuel Ledinot, Eric Nassor, et al.. ESTEREL: A formal method applied to avionic software development. Science of Computer Programming, Elsevier, 2000, 36 (1), pp.5-25. ⟨10.1016/S0167-6423(99)00015-5⟩. ⟨hal-00579632⟩



Record views