From HCI-AERO 2000: International Conference on Human-Computer Interaction in Aeronautics.
Edited by Kathy Abbott and Jean-Jacques Speyer and Guy Boy.
Toulouse, France.
September, 2000.
Pages 163–168.

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, finite-state 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.

@inproceedings{hci-aero00,
    AUTHOR = {Judy Crow and Denis Javaux (University of Liege) and John Rushby},
    TITLE = {Models and Mechanized Methods that Integrate Human Factors into Automation Design},
    BOOKTITLE = {{HCI-AERO} 2000: International Conference on Human-Computer Interaction in Aeronautics},
    YEAR = {2000},
    EDITOR = {Kathy Abbott and Jean-Jacques Speyer and Guy Boy},
    PAGES = {163--168},
    ADDRESS = {Toulouse, France},
    MONTH = {sep},
    URL = {http://www.csl.sri.com/papers/hci-aero00/}
}

• hci-aero00.doc
• hci-aero00.pdf
• hci-aero00.ps.gz