A Method for the Formal Verification of Human-interactive Systems

Abstract

Predicting failures in complex, human-interactive systems is difficult as they may occur under rare operational conditions and may be influenced by many factors including the system mission, the human operator's behavior, device automation, human-device interfaces, and the operational environment. This paper presents a method that integrates task analytic models of human behavior with formal models and model checking in order to formally verify properties of human-interactive systems. This method is illustrated with a case study: the programming of a patient controlled analgesia pump. Two specifications, one of which produces a counterexample, illustrate the analysis and visualization capabilities of the method.

Get full access to this article

View all access options for this article.

References

AOPA Air Safety Foundation (2007). 2007 Nall Report: Accident Trends and Factors for 2006. AOPA Air Safety Foundation. Available at http://www.aopa.org/asf/publications/07nall.pdf.

Bass

E.J.

Ernst-Fortin

S.T.

Small

R.L.

Hogans

J.T.

Jr. (2004). Architecture and development environment of a knowledge-based monitor that facilitate incremental knowledge-base development. IEEE Transaction on Systems, Man, and Cybernetics, Part A, 34(4), 441–449.

Baxter Heath Care Corporation (2006). Ipump pain management system operator's manual. Baxter Heath Care Corporation.

Blandford

Butterworth

Curzon

(2004) Models of interactive systems: A case study on programmable user modeling. International Journal of Human-computer Studies, 60(2), pp. 149–200.

Bolton

M. L.

Bass

E. J.

(2009a). Enhanced operator function model: A generic human task behavior modeling language. IEEE International Conference on Systems Man and Cybernetics, October 11–14, 2009, San Antonio, Texas.

Bolton

M. L.

Bass

E. J.

(2009b). Building a formal model of a human-interactive system: Insights into the integration of formal methods and human factors engineering. First NASA Formal Methods Symposium, April 6 - 8 Moffet Field, CA.

Bolton

M. L.

Bass

E. J.

Siminiceanu

R. I.

(2008). Using formal methods to predict human error and system failures. 2008 Applied Human Factors and Ergonomics International Conference, July 14–17, 2008, Las Vegas, NV.

Clarke

E. M.

Grumberg

Peled

(1999). Model Checking. MIT Press: Cambridge.

Clarke

E. M.

Wing

J.M.

(1996). Formal methods: State of the art and future trends. ACM Computing Surveys, 28(4):626–643.

10.

Crow

Javaux

Rushby

(2000). Models and mechanized methods that integrate human factors into automation design. International Conference on Human-Computer Interaction in Aeronautics, Toulouse, France.

11.

Curzon

Ruksenas

Blandford

(2007) An approach to formal verification of human-computer interaction. Formal Aspects of Computing. 513–550. DOI 10.10.1007/s00165-007-0035-6.

12.

Degani

(1996). Modeling human-machine systems: On modes, error, and patterns of interaction, Unpublished doctoral dissertation, Atlanta, GA: Georgia Institute of Technology.

13.

Degani

Heymann

Barshi

(2005). A formal methodology, tools, and algorithm for the analysis, verification, and design of emergency procedures and recovery sequences. NASA internal white paper. Mountain View, CA: NASA Ames Research Center.

14.

Fields

R. E.

(2001) Analysis of erroneous actions in the design of critical systems. D. Phil Thesis, Technical Report YCST 20001/09, University of York, Department of Computer Science.

15.

Hollnagel

(1993a). Human reliability analysis: Context and control. Academic Press.

16.

Hollnagel

, (1993b). The phenotype of erroneous actions. International Journal of Man-Machine Studies, 39, 1–32.

17.

Institute of Medicine. (2000). To Err Is Human: Building a Safer Health System. The National Academies Press.

18.

Javaux

(2002). A method for predicting errors when interacting with finite state systems. How implicit learning shapes the user's knowledge of a system. Reliability Engineering & System Safety, 75, 147–165.

19.

Moura

Owre

Shankar

, (2003). The SAL Language Manual. CSL Technical Report SRI-CSL-01-02 (Rev. 2).

20.

Paternò

(1999). Model-based Design and Evaluation of Interactive Applications. Springer Verlag.

21.

Perrow

(1984). Normal Accidents: Living with High-Risk Technologies. New York: Basic Books.

22.

Rushby

(1999). Using model checking to help discover mode confusions and other automation surprises. 3rd Workshop on Human Error, Safety, and System Development. Liege, Belgium, 7–8 June.

23.

Thurman

D. A.

Chappell

A. R.

Mitchell

C. M.

(1998). An enhanced architecture for OFMspert: A domain-independent system for intent inferencing. IEEE International Conference on Systems Man and Cybernetics.