As part of the FM?99 Technical Symposium, a tutorial will be entirely devoted to avionics systems. The 1990s are the decade when the digital avionics becomes a essential field of aeronautics. Digital avionics systems will constitute a critical and strategic element (the "brain") of future civil and military aircraft. They enable both technical performance improvement and cost reduction, but they also constitute one of the main elements of risk; their complexity stems for their critical, real time and highly distributed nature. The aim of this tutorial is to present both the industrial point of view and the academic solutions concerning the formal design, integration, verification and certification of digital avionics systems

This tutorial is composed of three half-day sessions respectively devoted to military systems, civil systems, and fault-tolerant and real-time analysis techniques.

Monday 20^th of Sept.
Session 1: civil avionics systems - problems and formal approaches
14:00 - 15:00     Civil avionics systems: an industrial point of view
                          Francois Pilarski - Aerospatial, Toulouse, France

15:15 - 16:15     LUSTRE: a functional language for designing data-flow critical systems
                          Nicolas Halwachs - Verimag, Grenoble, France

16:30 - 17h30     Asynchronous implementations of synchronous programs
                          Albert Benveniste - IRISA, Rennes, France
 

Tuesday 21^st of Sept.
Session 2: fault-tolerant and real-time analysis
10:00 - 10:45     ALTARICA: a language for designing and verifying fault-tolerant systems
                          Antoine Rauzy, LaBRI, Bordeaux, France

11:00 - 11:45     Application of the ALTARICA approach to avionics systems
                          Christel Seguin, ONERA, Toulouse, France

12:00 - 12:30     Modelling and verifying integrated modular avionics from a real-time point of view
                          Frederic Boniol, ONERA, Toulouse, France
 

Wednesday 22^nd of Sept.
Session 3: military avionics systems - problems and formal approaches
14:00 - 15:00     Developping avionic systems with Esterel at Dassault Aviation
                          Emmanuel Ledinot - Dassault-Aviation, Saint-Cloud, France

Esterel ,with its graphical editor SyncCharts by Simulog, is used to specify, simulate and verify reactive parts of mission management systems embedded in jet fighters. Examples of reactive modules are high level moding, man machine interfaces, landing gears control, fuel management etc. Object oriented extension of Esterel interfaced with UML-Rose by Rational Corp. have been developed to enhance reusability and productivity. Formal verification (model checking) is used either on safety critical functions or to reduce validation costs. Esterel has been used from 1989 to 1998 in an R&D context, and is now used operationally in the Mirage 2000-9 programme.

The Esterel programming language is dedicated to programming control-dominated reactive systems to be implemented in software or hardware. Esterel is textual, but the graphical SyncCharts formalism is fully compatible with it. The language is mathematically defined. The compiler generates either embeddable C code or a hardware netlist. It can also generate input for the verification system Xeve, which can prove program properties using symbolic reachability analysis techniques. Esterel is used by various companies for avionics, protocols, real-time process control, or circuit synthesis.

Contact: Frederic Boniol