Ariane
The goal of this case study was to validate the formal proof methodology on an example provided by EADS-Launcher. This example was a small part of the control/command of the Ariane V launcher, that was re-implemented in Lustre for this case study. Note that this software was not the one actually running within the launcher, but an experimental one, designed according to the same specifications. A set of safety properties, together with a set of environment assumptions were also provided.
We worked more specifically on the formalisation of the properties and the assumptions. Indeed, the whole verification process becomes irrelevant if properties and/or assumptions are wrong. In particular, the use of a simple language, based on regular expressions (Reglo) has greatly increased confidence in the validity of the assumptions.
Finally, we used the model-checker Lesar to check 36 safety properties. 12 of them appeared to be false because of a single bug in the design, that the Lesar diagnosis helped us to discover. Once this bug was fixed, Lesar was able to automatically prove all the properties in few minutes.
Airbus/ELMU
The ELMU controller is in charge of distributing the electrical load in the A380 aircraft. This is the case study that motivated the introduction of array iterators in Lustre. Using such iterators, the size of the ELMU system in Lustre was divided by 300 (from 300 000 to 1000 lines of code).
Gyroscope/Indian Aircraft industry
This case-study is a fault-tolerant system for the acquisition of gyroscopic data in a military aircraft. We used the Lustre programming environment for describing, simulating, and verifying this system. this work allowed us to show how the formalization of the requirements by means of an executable language allows ambiguities to be removed, and how the system can be developed step by step, while simulation and validation take place at each step. We believe that this example is representative of a wide class of embedded systems.
Snecma/Hispano-Suiza
Case studies have been made within the SAFEAIR 2 IST project in collaboration with Snecma/Hispano-Suiza . They used the automated testing tool Lurette in order to test an engine controller (M88). Several bugs were found, some them in the validated version of the controller. This work is described in [ISOLA 2004]
Renault/Regianov
Renault also used Lurette in the framework of the SAFEAIR 2 IST project. The case study consisted in testing a brake-by-wire system which aims at lowering the influences of the external conditions on the braking effect. For example, this systems allows retaining the same deceleration for the same brake pedal angle, even when the brake heats. This application made extensive use of non-linear functions over floats, and is therefore out-of-reach of current state-of-the-art formal verification tool. Lurette was used successfully to generate several millions of test sequences.
