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.


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

	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