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

https://hal-mines-paristech.archives-ouvertes.fr/hal-00579632
Contributor : Magalie Prudon <>
Submitted on : Thursday, March 24, 2011 - 2:34:16 PM
Last modification on : Monday, January 4, 2021 - 7:08:04 PM

Links full text

Identifiers

Citation

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⟩

Share

Metrics

Record views

588