An Experiment with the LOTOS Formal Description Technique on the Flight Warning Computer of Airbus 330/340 Aircrafts

Hubert Garavel and René-Pierre Hautbois

First AMAST International Workshop on Real-Time Systems (Iowa City, Iowa, USA), November 1993

Abstract:

This paper presents the main results of a two-year study concerning the introduction of formal methods in the life cycle of avionics software.
This study was done in the framework of the EUREKA European project AIMS (Aerospace Intelligent Management and development environment for embedded Systems). The ISO language LOTOS was used to describe a significant subset of the Flight Warning Computer of AIRBUS 330/340 aircrafts, which is a typical representative of Embedded Computer Systems. Six LOTOS descriptions were developed, (using both the abstract data types and the process algebra features of LOTOS) which are probably among the largest algebraic specifications written today. The CAESAR/ALDEBARAN toolset for LOTOS was used to support the description and analysis process. The LOTOS descriptions were automatically translated into executable prototypes, and then validated by means of simulation and testing.
The paper presents the techniques used and the results obtained. It ends with a critical evaluation of the ISO language LOTOS as far as other applications with similar characteristics are concerned.

20 pages

PDF

PostScript