Title
Using model checking to help discover mode confusions and other automation surprises
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 Murø state exploration system to a ‘kill-the-capture’ surprise in the MD-88 autopilot.
Year
DOI
Venue
2002
10.1016/S0951-8320(01)00092-8
Reliability Engineering & System Safety
Keywords
DocType
Volume
Automation surprise,Mode confusion,Model checking,Formal methods,Mental model,Human–computer interaction
Journal
75
Issue
ISSN
Citations 
2
0951-8320
31
PageRank 
References 
Authors
1.63
8
1
Name
Order
Citations
PageRank
John Rushby12459235.69