Flight Warning Computer (FWC) of Airbus 330-340 Aircrafts

Organisation:	AEROSPATIALE (Toulouse, France)
Method:	LOTOS
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Domain:	Embedded Computer Systems.
Period:	2 Years (1991-1993)
Size:	Six large LOTOS descriptions were developed, totaling more than 33,000 lines of LOTOS.
Description:	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 preliminary and detailed design are developed using an executable formal description technique. The correctness of the detailed design is established using computer-aided verification tools. The detailed design is automatically translated into executable code, using a compiler to perform the translation; the manual programming step is therefore suppressed. The unit testing phase can be suppressed if the compiler is proven. Since unit testing counts for 20-30% of the total software cost, significant savings are expected. The integration testing and validation steps are kept. To assess the feasibility of the approach, a typical ECS (the Airbus A330/340 Flight Warning Computer) was selected as a case-study. The corresponding software (traditionally implemented in Ada, PLM, and assembly language) was formally specified using the Formal Description Technique LOTOS. This resulted in six LOTOS descriptions totaling more than 33,000 lines. Using the CAESAR and CAESAR.ADT tools, two of the six descriptions (including the largest one) were successfully compiled into C code and partially verified on a number of test cases.
Conclusions:	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 community. 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.
Publications:	[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
Contact:	Hubert Garavel INRIA Rhone-Alpes 655 avenue de l'Europe 38330 Montbonnot Saint Martin France Tel: +33 4 76 61 52 24 Fax: +33 4 76 61 52 52 E-mail: Hubert.Garavel@inria.fr
Further Remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page