back icon
close icon

Capture phrases in quotes for more specific queries (e.g. "rocket ship" or "Fred Lynn")

Conference Paper  October 1, 2013

Example of a Complementary Use of Model Checking and Agent-Based Simulation

SRI Authors John Rushby

Citation

COPY

Gelman, G. E., Feigh, K. M., & Rushby, J. (2013, 13-16 October). Example of a complementary use of model checking and agent-based simulation. Paper presented at the IEEE International Conference on Systems, Man, and Cybernetics (SMC 2013), Manchester, UK.

Abstract

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. Such potential problems include automation surprises, which describe events when pilots are surprised by the actions of the automation. In this work, agent-based, hybrid time simulation and model checking are combined and their respective advantages leveraged in an original manner to find problematic human-automation interaction (HAI) early in the design process. The Tarom 381 incident involving the former Airbus automatic speed protection logic, leading to an automation surprise, was used as a common case study for both methodology validation and further analysis. Results of this case study show why model checking alone has difficulty analyzing such systems and how the incorporation of simulation can be used in a complementary fashion. The results indicate that the method is suitable to examine problematic HAI, such as automation surprises, allowing automation designers to improve their design.

How can we help?

Once you hit send…

We’ll match your inquiry to the person who can best help you. Expect a response within 48 hours.

Our Privacy Policy