Publications

State Event Models for the Formal Analysis of Human-Machine Interactions

Authors
Sébastien Combéfis, Dimitra Giannakopoulou, Charles Pecheur
Tags
, , ,
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 Tags: , , ,

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},
  }