TY  - JOUR
PY  - 2009//
TI  - A method for the formal verification of human-interactive systems
JO  - Proceedings of the Human Factors and Ergonomic Society annual meeting
A1  - Bolton, Matthew L.
A1  - Bass, Ellen J.
SP  - 764
EP  - 768
VL  - 52
IS  - 12
N2  - 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.<p />  <p>Language: en</p>
LA  - en
SN  - 2169-5067
UR  - http://dx.doi.org/10.1518/107118109X12524442637309
ID  - ref1
ER  -