Formal Verification of Human-Automation Interaction

Abstract

This paper discusses a formal and rigorous approach to the analysis of operator interaction with machines. It addresses the acute problem of detecting design errors in human-machine interaction and focuses on verifying the correctness of the interaction in complex and automated control systems. The paper describes a systematic methodology for evaluating whether the interface provides the necessary information about the machine to enable the operator to perform a specified task successfully and unambiguously. It also addresses the adequacy of information provided to the user via training material (e.g., user manual) about the machine's behavior. The essentials of the methodology, which can be automated and applied to the verification of large systems, are illustrated by several examples and through a case study of pilot interaction with an autopilot aboard a modern commercial aircraft. The expected application of this methodology is an augmentation and enhancement, by formal verification, of human-automation interfaces.

Get full access to this article

View all access options for this article.

References

Abbott, K. , Slotte, S. M. , & Stimson, D. K. (1996). The interface between flightcrews and modern flight deck systems. Washington, DC: Federal Aviation Administration.

Automated cockpits: Who's in charge? (1995a). Aviation Week and Space Technology, 142(5), 52–65.

Automated cockpits: Who's in charge? (1995b). Aviation Week and Space Technology, 142(6), 48–57.

Chappel, S. L. (1994). Using voluntary incident reports for human factors evaluations. In N. Johnston , N. McDonald , & R. Fuller (Eds.), Aviation psychology in practice (pp. 149–169). Hants, England: Avebury Technical.

Degani, A. , Heymann, M. , Meyer, G. , & Shafto, M. (2000). Some formal aspects of human-automation interaction (NASA Tech. Memorandum 209600). Moffett Field, CA: NASA Ames Research Center.

Degani, A. , Shafto, M. , & Kirlik, A. (1999). Modes in humanmachine systems: Constructs, representation, and classification. International Journal of Aviation Psychology, 9(2), 125–138.

Heymann M. , & Degani A. (2002). On abstractions and simplifications in the design of human-automation interfaces. (NASA Tech. Memorandum 2002-211397). Moffett Field, CA: NASA Ames Research Center.

Javaux, D. , & De Keyser, V. (1998). The cognitive complexity of pilot-mode interaction: A possible explanation of Sarter and Woods' classical result. In G. Boy , C. Graeber , & J. Robert (Eds.), Proceedings of the International Conference on Human-Computer Interaction in Aeronautics (pp. 49–54). Montreal, Canada: Ecole Polytechnique de Montreal.

Mellor, P. (1994). CAD: Computer aided disasters. High Integrity Systems, 1(2), 101–156.

10.

Norman, D. A. (1990). The “problem” with automation: Inappropriate feedback and interaction, not “over-automation.” Philosophical Transactions of the Royal Society of London, B 327, 585–593.

11.

Parasuraman, R. , Sheridan, T. B. , & Wickens, C. D. (2000). A model for the types and levels of human interaction with automation. IEEE Transaction on Systems, Man, and Cybernetics - Part A: Systems and Humans, 30(3), 286–297.

12.

Rouse, W. B. (Ed.). (1977). Applications of control theory in human factors - II [Special issue]. Human Factors, 19(5).

13.

Sarter, N. B. , & Woods, D. D. (1995). How in the world did I ever get into that mode? Mode error and awareness in supervisory control. Human Factors, 37, 5–19.

14.

Vicente, K. J. (1999). Cognitive work analysis. Mahwah, NJ: Erlbaum.

15.

Wickens, C. D. (1992). Engineering psychology and human performance. New York: Harper-Collins.

16.

Wiener, E. L. (1989). The human factors of advanced technology (“glass cockpit”) transport aircraft (NASA Contractor Report 177528). Moffett Field, CA: NASA Ames Research Center.

17.

Wiener, E. L. (1993). Crew coordination and training in the advanced-technology cockpit. In E. L. Wiener , B. G. Kanki , & R. L. Helmreich (Eds.), Cockpit resource management (pp. 199–226). San Diego: Academic.

18.

Wiener, E. L. , Chute, R. D. , & Moses, J. H. (1999). Transition to glass: Pilot training for high-technology transport aircraft (NASA Contractor Report 208784). Moffett Field, CA: NASA Ames Research Center.

19.

Woods, D. , Sarter, N. , & Billings, C. (1997). Automation surprises. In G. Salvendy (Ed.), Handbook of human factors and ergonomics (pp. 1926–1943). New York

John Wiley