Journal article
A Systematic Approach to Model Checking Human-Automation Interaction Using Task Analytic Models
IEEE transactions on systems, man and cybernetics. Part A, Systems and humans, v 41(5), pp 961-976
Sep 2011
Abstract
Formal methods are typically used in the analysis of complex system components that can be described as "automated" (digital circuits, devices, protocols, and software). Human-automation interaction has been linked to system failure, where problems stem from human operators interacting with an automated system via its controls and information displays. As part of the process of designing and analyzing human-automation interaction, human factors engineers use task analytic models to capture the descriptive and normative human operator behavior. In order to support the integration of task analyses into the formal verification of larger system models, we have developed the enhanced operator function model (EOFM) as an Extensible Markup Language-based, platform- and analysis-independent language for describing task analytic models. We present the formal syntax and semantics of the EOFM and an automated process for translating an instantiated EOFM into the model checking language Symbolic Analysis Laboratory. We present an evaluation of the scalability of the translation algorithm. We then present an automobile cruise control example to illustrate how an instantiated EOFM can be integrated into a larger system model that includes environmental features and the human operator's mission. The system model is verified using model checking in order to analyze a potentially hazardous situation related to the human-automation interaction.
Metrics
Details
- Title
- A Systematic Approach to Model Checking Human-Automation Interaction Using Task Analytic Models
- Creators
- M. L Bolton - Nat. Aeronaut. & Space Adm. Ames Res. Center, San Jose State Univ. Res. Found., Moffet Field, CA, USAR. I Siminiceanu - Nat. Inst. of Aerosp., Hampton, VA, USAE. J Bass - Dept. of Syst. & Inf. Eng., Univ. of Virginia, Charlottesville, VA, USA
- Publication Details
- IEEE transactions on systems, man and cybernetics. Part A, Systems and humans, v 41(5), pp 961-976
- Publisher
- IEEE
- Resource Type
- Journal article
- Language
- English
- Academic Unit
- Information Science
- Web of Science ID
- WOS:000294134300013
- Scopus ID
- 2-s2.0-80052064283
- Other Identifier
- 991014878574904721
InCites Highlights
Data related to this publication, from InCites Benchmarking & Analytics tool:
- Collaboration types
- Domestic collaboration
- Web of Science research areas
- Computer Science, Cybernetics
- Computer Science, Theory & Methods