Database of Case Studies Achieved Using CADP

Air Traffic Control (ATC) System.

Organisation: Department of Computing, University of Glasgow (SCOTLAND)

Method: LOTOS

Tools used: CADP (Construction and Analysis of Distributed Processes)

Domain: Embedded Systems.

Period: 1999.

Size:

Description: An important aspect in the development of safety critical systems is the creation of the user interface. This study describes a prototyping environment for building complex, concurrent multi-user systems in a high-level, structured manner. The environment allows also to derive automatically a LOTOS specification from the prototype system, thus opening the way to formal analysis using appropriate verification tools such as CADP. It is demonstrated how the prototyping environment has been used to construct a prototype data-link Air Traffic Control (ATC) system and how the formal verification carried out with CADP allowed to discover a number of small but potentially important problems in the ATC prototype system.

The prototyping environment combines the advantages of standard visual programming and high-level specifications. First, the static components of an interface are produced visually using an interface builder, and then a structured architecture is derived and developed. The components are described using a high-level declarative language, in terms of user actions changing a shared state. The prototyping system is embedded in Haskell and uses a binding to Tcl-Tk in order to provide a widget library.

The architecture of the ATC system is structured as a tree of components, each one representing an interaction object, and the structure representing the hierarchical display of the resulting interface. The Simulator consists of a set of Controller Views, which in turn consist of: a radar area showing all aircraft; a Messages In and a Messages Out window showing received and sent data-link messages; a Flight Data Plan window; a Data Link Messages window; a Configure window allowing controllers to modify certain aspects of the appearance of their screen; and an Aircraft Display window.

The development environment provides a translator of the prototype system description into a LOTOS specification, which is suitable for formal analysis using the CADP toolset. The tools CAESAR, ALDEBARAN, and PROJECTOR have been used in order to generate compositionally the LTS model corresponding to the tree structure of the ATC system. The ATC prototype system has been analysed w.r.t. each of the three major underlying communication protocols: transfer between sectors, negotiation of transfer parameters, and flight clearances.

A mixture of interactive simulation and model-checking with the EVALUATOR tool has been used to carry out the analysis. This allowed to discover several problems in the specification that occurred under error or time out conditions. In particular, this allowed to detect a situation when (after a bad sequencing of messages) the system continues to wait for a hypothetical reply and does not display any more message to the controller.

Conclusions: The ability to derive a formal specification from a prototype description of a multi-user system is important for ensuring the robustness of the system. Used in connection with dedicated analysis tools like CADP, it allows to formally reason about complex areas of the system, such as moded behaviour resulting from communication protocols. The approach has proved effective in the development of a complex ATC data-link prototype.

Publications: [Sage-Johnson-99-a] M. Sage and C. W. Johnson. "A Declarative Prototyping Environment for the Development of Multi-User, Safety-Critical Systems". Proceedings of the 17th International System Safety Conference ISSC'99 (Orlando, Florida, USA), August 1999.

[Sage-Johnson-99-b] M. Sage and C. W. Johnson. "Formally Verified Rapid Prototyping for Air Traffic Control". Proceedings of the 3rd Workshop on Human Error, Safety and Systems Development (Liege, Belgium), 1999.

[Sage-Johnson-02] M. Sage and C. W. Johnson. "Formally Verified Rapid Prototyping for Air Traffic Control". Reliability Engineering and System Safety, vol. 75, num. 2, pages 121-132, 2002.
Available on-line at: https://doi.org/10.1016/S0951-8320(01)00089-8

Contact:
Chris Johnson
Department of Computing Science
University of Glasgow
Glasgow
G12 8QQ
SCOTLAND
Tel: +44 141 330 6053
Fax: +44 141 330 4913
E-mail: johnson@dcs.glasgow.ac.uk
Further remarks: This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Last modified: Wed Apr 20 16:20:42 2022.

Back to the CADP case studies page