Designing Interactive Applications for Air Traffic Control with the Support of MEFISTO
Keywords
Formal Methods, Air Traffic Control, Design Process, Interactive Safety-Critical Applications, Usability testing.
INTRODUCTION
This short paper presents an overview of the approach developed within the MEFISTO project. An important element in the approach is the use of formal models and their integration with other, less formal, techniques.
MEFISTO (Modelling, Evaluating and Formalising Interactive Systems using Tasks and interaction Objects) is a European Commission IVth Framework Reactive Long Term Research Esprit project. Its main goal is to investigate how the use of formal techniques can be introduced into the design of interactive safety-critical systems, such as Air Traffic Control applications (ATC). Also important is the evaluation of the design notations, computer support tools and the developed ATC prototypes. This type of application engenders an integrated satisfaction of both usability and safety requirements, as in some circumstances a human error can threaten human life. This means that the design of the interactive ATC environments provided to controllers requires the use of rigorous techniques and systematic methods that allow designers to identify possible problematic situations in advance and help in providing support to the end users. In addition, the use of formal techniques can provide precise documentation and can support representations of design rationale.
To make the use of formal models more affordable, in MEFISTO we have paid particular attention to the use of software tools in order to ease their development and analysis, so yielding useful information for the designers in various phases of the design process.
However, we are aware that formal techniques cannot cover all the needs in the design cycle. Thus, it is important to understand what other informal techniques should be used and how their integration with formal approaches should be carried out.THE MEFISTO INGREDIENTS
Critical choices in the project were the selection of the formal notations employed to represent and analyse the models and the case studies where the notations were applied. We have used a couple of notations developed by MEFISTO partners: the ConcurTaskTrees notation (CTT) [1] to represent task models and the Interactive Cooperative Objects (ICO) notation [2] for system models.
ConcurTaskTrees
ConcurTaskTrees is a notation for task model specifications which has been developed to overcome limitations of notations previously used in this field. Its main purpose is to be an easy-to-use notation that can support the design of real industrial applications. The main features of ConcurTaskTrees are: hierarchical structure, graphical representation of the model, rich set of temporal operators among tasks, focus on activities, and support for description of multi-user co-operations.
Interactive Cooperative Objects
The ICO formalism uses concepts borrowed from the object-oriented approach (dynamic instantiation, classification, encapsulation, inheritance, client/server relationship) to describe the structural or static aspects of systems, and uses high-level Petri nets to describe their dynamic or behavioural aspects.
ICOs were originally devised for the modelling and implementation of event-driven interfaces. Using this formalism it is possible to formally describe all the components of an interactive application as well as verifying properties on the specification.Integrating Formal And Informal Methods
An important aspect of MEFISTO is also to precisely define the way in which formal description methods (used for describing requirements, tasks and system) can be integrated with more classical informal methods for the design of interactive systems. To this end informal methods such as story telling, scenarios, deviation analysis and usability testing have been investigated and refined to fit MEFISTO objectives.
Case Study Selection
The case studies are used to apply the methods and techniques for user interface design and evaluation developed in the project in order to verify and evaluate their utility and innovation with respect to current design practice. In Air Traffic Control, each phase of a flight requires specific control systems and applications. Each application raises particular requirements for its user interface design. Moreover, the use of different technologies can introduce additional issues from a usability and safety point of view.
The case studies have been selected in order to raise complementary issues that allow the project to have a good view of the possible usability and safety problems to be solved when designing safety critical real-time work support systems. Two MEFISTO case studies have been identified:
In both cases studies we addressed the problem of designing new interactive environments able to support data link communication in addition to traditional VHF radio.
TOOLS FOR FORMAL MODELS
One of the strengths of the approach developed is the use of automatic tools for supporting the formal notations. Developing a formal model can be a long process, which requires a considerable effort. Automatic tools can ease such activity and can help designers to get information from the models, which is useful for supporting the design cycle. In MEFISTO two tools have been used. CTTE (ConcurTaskTrees Environment) is a public available tool (downloadable from http://giove.cnuce.cnr.it/ctte.html) that allows designers to develop task models for cooperative applications specified in the ConcurTaskTrees notation. The tool has various features supporting editing of task models. It can automatically check the syntax of the specification, give statistical information, compare task models, simulate their behaviour and give examples of scenarios of use.
PetShop [3] is a tool that allows the editing of ICO diagrams, to simulate their behaviour and to connect with the user interface implementation.CONCLUSIONS
Our approach in MEFISTO has rather ambitious goals. While it is unlikely that we can completely reach all of them, we feel that considerable results have been produced that can be useful for other projects.
Large specifications of real systems have been carried out showing the possible scalability of the CTT and ICO notations, whilst the support of automatic tools allows designers to better develop and use such specifications.
Two real prototypes have been developed and further improvements are planned once the evaluation phase is complete. While the use of task models has been shown to be useful in supporting the design phase, the use of system models has been demonstrated to be particularly useful in documenting the system implementation of high-fidelity prototypes that can be input into the final production phase. Even though the use of these formal techniques represents a useful improvement to current practice in order to reach a systematic support for design, documentation, and evaluation, it is clear that they have to be integrated with informal techniques in order to have a complete method. For example, scenarios are a useful means in supporting various phases of the design cycle, as they are effective in highlighting specific issues.
ACKNOWLEDGMENTS
We gratefully acknowledge support from the European Commission, DG3 ESPRIT LTR programme. MEFISTO web site http://giove.cnuce.cnr.it/mefisto.html
REFERENCES AND PROJECT BIBLIOGRAPHY