Example of a Complementary Use of Model Checking and Human Performance Simulation

Aircraft automation designers are faced with the challenge to develop and improve automation such that it is transparent to the pilots using it. To identify problems that may arise between pilots and automation, methods are needed that can uncover potential problems with automation early in the design process. In this paper, simulation and model checking are combined and their respective advantages leveraged to find problematic human-automation interaction using methods that would be available early in the design process. A particular problem of interest is automation surprises, which describe events when pilots are surprised by the actions of the automation. The Tarom flight 381 incident involving the former Airbus automatic speed protection logic, leading to an automation surprise, is used as a common case study. Results of this case study indicate that both methods identified the automation surprise found in the Tarom flight 381 incident, and that the simulation identified additional automation surprises associated with that flight logic. The work shows that the methods can be symbiotically combined, and the joint method is suitable to identify problematic human-automation interaction such as automation surprise.