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.
Abstract
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
@article{Rushby:RESS02,
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