A formal method for including the probability of erroneous human task behavior in system analyses

Formal methods have been making inroads into the engineering of human-automation interaction (HAI) by allowing engineers to use mathematical proofs to determine whether normative or unanticipated erroneous human behavior can ever cause problems. However, these approaches are limited because they do not give engineers a way to assess the relative likelihood of different outcomes. In this work, we address this shortcoming by defining a new approach that combines formal approaches with human reliability analysis and probabilistic and statistical model checking. This approach ultimately allows analysts to compute the probability of different outcomes occurring in reactive HAI systems. We describe how this method was realized, assess its scalability, and demonstrate its capabilities with an automated teller machine example. We ultimately discuss our results and describe directions of future research.

Automated summary

The study introduces a new method that combines formal methods with human reliability analysis, probabilistic and statistical model checking to compute the probability of different outcomes in reactive human-automation interaction systems. The method is demonstrated with an automated teller machine example, and future research directions are discussed.