State Event Models for the Formal Analysis of Human-Machine Interactions
- Title
- State Event Models for the Formal Analysis of Human-Machine Interactions
- Authors
- Sébastien Combéfis?, Dimitra Giannakopoulou, Charles Pecheur
FM2018 Δ | 0Kb | 28 May 2020 |
Fmics2013 Δ | 0Kb | 28 May 2020 |
GandALF2017 Δ | 0Kb | 28 May 2020 |
HMI2011 Δ | 0Kb | 28 May 2020 |
LVLPrivate Δ | 0Kb | 28 May 2020 |
LVLPrivateNews Δ | 0Kb | 28 May 2020 |
Main Δ | 0Kb | 28 May 2020 |
Members Δ | 0Kb | 28 May 2020 |
Publications Δ | 4Kb | 28 May 2020 |
Site Δ | 0Kb | 28 May 2020 |
Talks Δ | 4Kb | 28 May 2020 |
Tools Δ | 0Kb | 28 May 2020 |
- Type
- In Proceedings
- Book title
- Proceedings of AAAI Symposium on Formal Verification in Human-Machine Systems
- Publisher
- AAAI
- Editor
- Eric G. Mercer, Michael A. Goodrich, Neha Rungta, Ellen Bass
- Year
- 2014
Abstract
The work described in this paper was motivated by our experience with applying a framework for formal analysis of human-machine interactions (HMI) to a realistic model of an autopilot. The framework is built around a formally defined conformance relation called "full-control" between an actual system and the mental model according to which the system is operated. Systems are well-designed if they can be described by relatively simple, full-control, mental models for their human operators. For this reason, our framework supports automated generation of minimal full-control mental models for HMI systems, where both the system and the mental models are described as labelled transition systems (LTS). The autopilot that we analysed has been developed in the NASA Ames HMI prototyping tool ADEPT. In this paper, we describe how we extended the models that our HMI analysis framework handles to allow adequate representation of ADEPT models. We then provide a property-preserving reduction from these extended models to LTSs, to enable application of our LTS-based formal analysis algorithms. Finally, we briefly discuss the analyses we were able to perform on the autopilot model with our extended framework.
Tags: Human Computer Interaction, Verification, ADEPT, Project NASA
- BibTeX Record
@INPROCEEDINGS{lvl-2014-975903, TITLE = {State Event Models for the Formal Analysis of Human-Machine Interactions}, AUTHOR = {Sébastien Combéfis and Dimitra Giannakopoulou and Charles Pecheur}, YEAR = {2014}, PUBLISHER = {AAAI}, EDITOR = {Eric G. Mercer and Michael A. Goodrich and Neha Rungta and Ellen Bass}, URL = {https://lvl.info.ucl.ac.be/Publications/StateEventModelsForTheFormalAnalysisOfHuman-MachineInteractions}, }