A Systematic Approach to Model Checking Human–Automation Interaction Using Task Analytic Models
- 22 March 2011
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Systems, Man, and Cybernetics - Part A: Systems and Humans
- Vol. 41 (5), 961-976
- https://doi.org/10.1109/tsmca.2011.2109709
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.Keywords
This publication has 34 references indexed in Scilit:
- Formally verifying human–automation interaction as part of a system model: limitations and tradeoffsInnovations in Systems and Software Engineering, 2010
- A Method for the Formal Verification of Human-interactive SystemsProceedings of the Human Factors and Ergonomics Society Annual Meeting, 2009
- Formal and experimental validation approaches in HCI systems design based on a shared event B modelInternational Journal on Software Tools for Technology Transfer, 2006
- Counterexample-guided abstraction refinement for symbolic model checkingJournal of the ACM, 2003
- Augmenting the operator function model with cognitive operations: assessing the cognitive demands of technological innovation in ship navigationIEEE Transactions on Systems, Man, and Cybernetics - Part A: Systems and Humans, 2000
- Users as rational interacting agents: formalising assumptions about cognition and interactionPublished by Springer Science and Business Media LLC ,1997
- Formal methodsACM Computing Surveys, 1996
- Using GOMS for user interface design and evaluationACM Transactions on Computer-Human Interaction, 1996
- The UAN: a user-oriented representation for direct manipulation interface designsACM Transactions on Information Systems, 1990
- Statecharts: a visual formalism for complex systemsScience of Computer Programming, 1987