Presented a framework for automatic discovery of mode confusions in software used for simulations of aircraft and shuttle automation. We demonstrated our approach on the example of a Web-based autopilot tutorial used at NASA for pilot training. The main approach is to identify the four models of the system: the machine, the interface, the user, and the user task. The user task is described as a collection of sequences of actions performed on the display using regular expressions notation. The code for the user task is generated automatically. The user task plays the role of a driver that synchronously executes the remaining models in the system. JPF is used to go through all of the executions of the task and to check the consistency of the states across the models. If one of the models goes into a state that belongs to a different "specification class" than the others, JPF records the faulty execution. We implemented a script that analyzes a JPF counterexample and produces a trace in terms of the actions that the user performs on the display.
Using code level model checking to discover automation surprises
2002-01-01
876224 byte
Conference paper
Electronic Resource
English
Supporting Event Prediction for Level 2 ADAS Users to Prevent Automation Surprises
Springer Verlag | 2021
|Oops, "It Didn't Arm." A Case Study of Two Automation Surprises
British Library Conference Proceedings | 1995
|