Department of Computing, University of Glasgow (SCOTLAND)
CADP (Construction and Analysis of Distributed Processes)
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 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.
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.
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.
Available online at: http://www.dcs.gla.ac.uk/~meurig/research/isscpaper.html
Department of Computing Science
University of Glasgow
Tel: +44 141 330 6053
Fax: +44 141 330 4913
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|