Formal Models for Cooperative Tasks: Concepts and an Application for En-Route Air Traffic Control
This paper presents a proposal for specifying task models for cooperative applications that allow designers to describe the relationships between the activities performed by various users involved in cooperative environments. To this end we extend the Con
- PDF / 1,972,739 Bytes
- 16 Pages / 482 x 692 pts Page_size
- 41 Downloads / 196 Views
(2)
CNUCE-C.N.R., Pisa, Italy CENA, Toulouse, France
12)
Abstract. This paper presents a proposal for specifying task models for cooperative applications that allow designers to describe the relationships between the activities performed by various users involved in cooperative environments. To this end we extend the ConcurTaskTree notation so that new information useful for describing complex cooperative applications can be clearly specified. An example of application to describe En-Route Air Traffic Control (ATC) is given to illustrate and clarify our approach.
1 Introduction Formal methods are based on the use of notations with a precise semantics that allow designers to clarify many aspects, remove ambiguities in their specifications, and develop rigorous reasoning about the properties of these specifications. However, both learning and applying formal methods is time-consuming. We believe that these costs are motivated when designers consider applications where a bad design can generate heavy consequences. Safety critical applications [6] are an interesting application area where the current user interfaces need to be improved, as demonstrated by several studies which show how most accidents are predominantly due to human errors and the need to improve their analysis [4]. It is thus important to develop a formal analysis of user interfaces for these applications [5] in order to have a full understanding of the possible effects of user interactions. One of the most interesting results of the application of formal methods in the HeI field [9] is that precise descriptions of task models [7,10,13] can be given. Thus it is important to have a rich set of temporal operators and to define a precise semantics which can explain the behaviour described when these operators are composed in complex expressions. In the European MEFISTO Project we aim to develop formal task models to improve the analysis and the design of safety critical interactive applications. We started by considering a case study consisting of an application for air traffic control during the en-route phase.
P. Markopoulos et al. (eds.), Design, Specification and Verification of Interactive Systems ’98 © Springer-Verlag Wien 1998
72
We soon realised that besides being a safety-critical application because an error caused by the controller can have serious consequences, it is also a highly cooperative application. In fact, for each sector there is one strategic controller and one executive controller, who communicate with each other and, in the application currently used, the executive controller communicates with the pilots, and the strategic controller communicates with the strategic controllers of the other neighbouring sectors. This raises the need for an integrated analysis of usability, safety and cooperative aspects in the design of user interfaces for these applications. In fact, many of the possible safety and usability problems are related to how the various users cooperate with each other to reach common goals. In the design of comple
Data Loading...
