Designing interactive applications for air traffic control with the support of MEFISTO

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.