Checking formal verification models for human-automation interaction

In complex human-machine systems, unforeseen failures in the interaction between human agents, automation and the environment provide an important contribution to incidents and accidents. The complexity of many systems precludes a designer from foreseeing all possible states of interaction. Formal verification methods are explored as a means of making human-machine systems more robust against failures arising from these unforeseen interactions. For these methods, a analytic model of the operator task is combined with a formal model of the system (automation), and, using model checking tools, a formal verification of the interaction is performed. Validity of the results, however, does require a sufficient correspondence between the model and the actual system. To validate this correspondence, this study explores an approach where the predictions from a formal model are compared to behavior of the human-machine system. The Paparazzi UAV ground control station is used as a test case, and a framework was created to automatically play back results from the formal verification tool to the UAV ground control simulation. The results show a good correspondence between the actual system and the model results, even if the model is by necessity a simplified description of actual system behavior. A remaining problem is creating enough variation in verification tool traces to properly test the correspondence between the formal model and the system.