Models and Mechanized Methods that Integrate Human Factors into Automation Design
Judith Crow, Denis Javaux, John Rushby · 2000
Recent work has shown a convergence between the Human Factors and Formal Methods communities that opens promising new directions for collaborative work in calculating, predicting, and analyzing the behavior of complex aeronautical systems and their operators. Previously it has been shown that fully automatic, finitestate verification techniques can be used to identify likely sources of mode confusion in existing systems; in this paper we focus on use of these techniques in the design of new systems. We use a simple example to demonstrate how automated finite-state techniques can be used to explore autopilot design options, and then suggest additional applications for this technique, including the validation of empirically-derived, minimal mental models of autopilot behavior. KEYWORDS Human factors, formal methods, finite-state machines, automation, design MODELS, METHODS, AND MECHANIZATION Research in aviation psychology and in human factors (HF) has provided valuable insights and ...