Citation

Bolton ML, Bass EJ. Proc. Hum. Factors Ergon. Soc. Annu. Meet. 2009; 52(12): 764-768.

Affiliation

University of Virginia, Systems and Information Engineering, Charlottesville, Virginia.

Copyright

(Copyright © 2009, Human Factors and Ergonomics Society, Publisher SAGE Publishing)

DOI

10.1518/107118109X12524442637309

PMID

21572977

PMCID

PMC3092305

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.

Language: en