Generating Erroneous Human Behavior From Strategic Knowledge in Task Models and Evaluating Its Impact on System Safety With Model Checking

Human-automation interaction, including erroneous human behavior, is a factor in the failure of complex, safety-critical systems. This paper presents a method for automatically generating formal task analytic models encompassing both erroneous and normative human behavior from normative task models, where the misapplication of strategic knowledge is used to generate erroneous behavior. Resulting models can be automatically incorporated into larger formal system models so that safety properties can be formally verified with a model checker. This allows analysts to prove that a human-automation interactive system (as represented by the formal model) will or will not satisfy safety properties with both normative and generated erroneous human behavior. Benchmarks are reported that illustrate how this method scales. The method is then illustrated with a case study: the programming of a patient-controlled analgesia pump. In this example, a problem resulting from a generated erroneous human behavior is discovered. The method is further employed to evaluate the effectiveness of different solutions to the discovered problem. The results and future research directions are discussed.