AEROSPATIALE (Toulouse, France)
CADP (Construction and Analysis of Distributed Processes)
Embedded Computer Systems.
2 Years (1991-1993)
Six large LOTOS descriptions were developed, totaling more than 33,000
lines of LOTOS.
This study was done in the framework of the European project Eureka/AIMS.
It was conceived to reduce the high cost of Embedded Critical Systems (ECSs)
by introducing formal methods in the ECS development process. This project
studied the feasibility of a software life cycle different from the traditional
one. In the proposed approach:
The results of this study were balanced. On one hand, this case-study
demonstrated that large LOTOS descriptions (approx. 13,000 lines) written in
an industrial context could be successfully compiled and executed. This
order of magnitude had not been reached before in the process algebra
However, from an industrial point of view, it appeared that the approach could not replace the traditional ECS development process. The main reason for this was the lack of provably-correct compilers, capable of translating formal descriptions into Ada or PLM code to be certified and embedded.
Although the objectives of this study were probably too ambitious for the current state of art in formal methods, the principles were sound: formal methods, verification techniques, and automatic code generation could be profitably introduced in the ECS development process.
[Garavel-Hautbois-93] Hubert Garavel and Rene-Pierre Hautbois.
An Experiment with the Formal Description in LOTOS of the Airbus A340
Flight Warning Computer. In Maurice Nivat, Charles Rattray, Teodor Rus,
and Giuseppe Scollo, editors, First AMAST International Workshop on
Real-Time Systems (Iowa City, Iowa, USA), November 1993.
[Garavel-Hautbois-94] Hubert Garavel and Rene-Pierre Hautbois. Experimenting LOTOS in Aerospace Industry. In Teodor Rus and Charles Rattray, Theories and Experiences for Real-Time System Development, chapter 11. World Scientific, Amast Series in Computing vol. 2, 1994
Available on-line from http://cadp.inria.fr/publications/Garavel-Hautbois-93.html
and from the CADP Web site in PDF or PostScript
655 avenue de l'Europe
38330 Montbonnot Saint Martin
Tel: +33 4 76 61 52 24
Fax: +33 4 76 61 52 52
|Further Remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|