Using code level model checking to discover automation surprises

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.