Example of a Complementary Use of Model Checking and Human Performance
Simulation
Gabriel Gelman, Karen M. Feigh, and John Rushby
IEEE Transactions on Human-Machine Systems, October 2014, pp 576-590.
Abstract
Aircraft automation designers are faced with the challenge to develop
and improve automation such that it is transparent to the pilots using
it. To identify problems that may arise between pilots and automation,
methods are needed that can uncover potential problems with automation
early in the design process. In this paper, simulation and model
checking are combined and their respective advantages leveraged to
find problematic human-automation interaction using methods that would
be available early in the design process. A particular problem of
interest is automation surprises, which describe events when pilots
are surprised by the actions of the automation. The Tarom flight 381
incident involving the former Airbus automatic speed protection logic,
leading to an automation surprise, is used as a common case
study. Results of this case study indicate that both methods
identified the automation surprise found in the Tarom flight 381
incident, and that the simulation identified additional automation
surprises associated with that flight logic. The work shows that the
methods can be symbiotically combined, and the joint method is
suitable to identify problematic human-automation interaction such as
automation surprise.
Link to the paper at
IEEE Xplore
Citations
from Google scholar
BibTeX Entry
@ARTICLE{Gelman-etal:THMS2014,
AUTHOR = {Gabriel Gelman and Karen Feigh and John Rushby},
TITLE = {Example of a Complementary use of Model Checking
and Human Performance Simulation},
JOURNAL = {IEEE Transactions on Human-Machine Systems},
YEAR = 2014,
VOLUME = 44,
NUMBER = 5,
PAGES = {576--590},
MONTH = oct
}
Having trouble reading our papers?
Return to John Rushby's bibliography page
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page