Task oriented modelling of devices-the air traffic control domain

A method is given that specifies software systems taking into consideration the tasks users will perform on these systems, i.e. a method which is task oriented. The authors extend the task knowledge structure theory (TKS) of task modelling by defining a formal framework for modeling users´ tasks; they then derive the formal specification of the interactive system in terms of the (formal) model of the task the system is supposed to support. The formal method proposed, was arrived at using `backward engineering´: the authors want to specify interactive systems in a particular way, so they find a method for formalising users´ task requirements that can guide them (using appropriate heuristics) to the desired system specification. They use examples from the domain of air traffic control, using a hypothetical electronic flight strip system. Specifying a system is a typical situation where one has some notion of `state´, together with some operations for `interrogating´ and `updating´ the state. There are two approaches to specifying such a situation. Using a constructive approach, one defines directly the set of states together with functions for various operations. Using the axiomatic (also called algebraic) approach, one does not define particular sets and functions, but merely indicates the interaction between the operations. Sets of axioms convey how operations interact. The authors have chosen the axiomatic approach for their formalisms