Evaluating human-automation interaction using task analytic behavior models, strategic knowledge-based erroneous human behavior generation, and 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 task analytic models encompassing both erroneous and normative human behavior from normative task models by manipulating modeled strategic knowledge. Resulting models can be automatically translated 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. This method is 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 and a potential solutions is explored. Future research directions are discussed.