Using Model Checking to Help Discover Mode Confusions and Other Automation Surprises

John Rushby

Presented at the The 3rd Workshop on Human Error, Safety, and System Development (HESSD'99), Liege, Belgium, 7--8 June 1999 and published in Reliability Engineering and System Safety, vol. 75, no. 2, pp. 167--177, Febuary 2002.


Automation surprises occur when an automated system behaves differently than its operator expects. If the actual system behavior and the operator's "mental model" are both described as finite state transition systems, then mechanized techniques known as "model checking" can be used automatically to discover any scenarios that cause the behaviors of the two descriptions to diverge from one another. These scenarios identify potential surprises and pinpoint areas where design changes, or revisions to training materials or procedures, should be considered. The mental models can be suggested by human factors experts, or can be derived from training materials, or can express simple requirements for "consistent" behavior. The approach is demonstrated by applying the Murphi state exploration system to a "kill-the-capture" surprise in the MD-88 autopilot.

This approach does not supplant the contributions of those working in human factors and aviation psychology, but rather provides them with a tool to examine properties of their models using mechanized calculation. These calculations can be used to explore the consequences of alternative designs and cues, and of systematic operator error, and to assess the cognitive complexity of designs.

The description of model checking is tutorial and is hoped to be accessible to those from the human factors community to whom this technology may be new.

Download the full paper:

Journal version: gzipped postscript, PDF (Adobe Acrobat)

Original version: gzipped postscript, postscript, PDF (Adobe Acrobat), or PDF (Adobe Acrobat) A4 size,

Slides: gzipped postscript, postscript,

Murphi Files

These are the sources that generated the output appearing in the numbered figures in the paper. Download them as source files, compile with Murphi (available here) to yield (e.g.,) the binary file fig1 and then do fig1 -tv. Lines beginning with -- are comments in Murphi and are used to make it easier to see what's changed from one file to the next

BibTeX Entry

        AUTHOR = {John Rushby},
        TITLE = {Using Model Checking to Help Discover Mode Confusions
                and Other Automation Surprises},
        JOURNAL = {Reliability Engineering and System Safety},
        PAGES = {167--177},
        VOLUME = 75,
        NUMBER = 2,
        MONTH = feb,
        YEAR = 2002

Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page