Application name:

CIDS A330/340 Cabin Communication System

Organisation:

DST Deutsche System-Technik GmbH and JP Software-Consulting, Kiel, Germany

Method:

Z in combination with (semi-formal) structured design techniques (Ward/Mellor style).

Tools:

DST Z-Toolbox

Domain:

Air traffic control/management

Period:

1992 - 1994: the system is now operational in the Airbus A330/340. The application described is one of about 20 applications integrated in the full system. It required an effort of approximately one man-year, including specification, design, coding, integration, testing and verification efforts.
1995: Testing case study

Size:

The formal specification consists of 1500 lines of Z. The implementation consists of 6000 lines of C.

Description:

The cabin illumination system is an application function of the Cabin Intercommunication Data System (CIDS) that contains all cabin communication functions of the new Airbus family A330/340. About 20 application functions are implemented in CIDS, such as the telephone communication system, the public address system and control of various cabin sensors. The CIDS system's criticality level according to the RTCA DO178B standard is B (A is the highest, D the lowest criticality level).

The cabin illumination application implements the control functions for the illumination units installed in the aircraft cabin, such as switching and dimming the illumination in cabin zones, entry areas etc. Moreover, the application controls some `mildly' safety-critical functions. E.g. in case of cabin decompression, all illumination units must be automatically switched on. In 1995 the SW integration test process for the CIL application has been repeated as part of a case study. Here, the DST Z-Toolbox was used for automatic test class generation and automatic test result evaluation.

Conclusions:

Conventional CASE methods turned out to be insufficient to tackle the more complex functions of a safety-critical application system. This problem can be overcome by combining CASE methods with formal specification and verification methods. We regard the application of Z as an important factor for the successful completion of the CIDS applications developed by DST. It did not only provide a technique to develop trustworthy specifications, but also helped to reduce the costs for implementation and integration, because the specification allowed to derive a software design with minimum complexity.

The experiences from the test automation case study carried out after the main project were very positive. It was demonstrated, that it is possible to supply a high degree of automation for the testing process based on a Z specification.

Publications:

"The Airbus A330/340 Cabin Communication System ". Ute Hamer and Jan Peleska. In: Applications of Formal Methods, edited by Michael G. Hinchey and Jonathan Bowen. Prentice Hall International, Series in Computer Science. 1995.

"Improving Software Tests using Z Specifications". Hans-Martin Hoercher. In: Proceedings of the Z User Meeting - ZUM'95. Springer Verlag, Lecture Notes in Computer Science, no. 967. Pages 152-166. September 1995.

"Using Formal Specifications to support Software Testing". Hans-Martin Hoercher and Jan Peleska. Software Quality Journal 1995(4)4: 309-327.

Contact:

Name:	Hans-Martin Hoercher
Organisation:	DST Deutsche System-Technik GmbH
Address:	Edisonstrasse 3 D-24145 Kiel
Country:	Germany
Phone number:	+49 (431) 710
Fax:	+49 (431) 7109503
E-mail:	hoercher@dst.de

Contact:

Name:	Jan Peleska
Organisation:	JP Software-Consulting
Address:	Goethestrasse 26 D-24116 Kiel
Country:	Germany
Phone number:	+49 (431) 552882
Fax:	+49 (431) 552892
E-mail:	jap@informatik.uni-bremen.de

© copyright 2004 | Formal Methods Europe