Publications

A Formal Framework for Design and Analysis of Human-Machine Interaction

Authors
Sébastien Combéfis, Dimitra Giannakopoulou, Charles Pecheur, Michael Feary
Tags
, , , , ,
Title
A Formal Framework for Design and Analysis of Human-Machine Interaction
Authors
Sébastien Combéfis, Dimitra Giannakopoulou, Charles Pecheur, Michael Feary
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
2011 IEEE International Conference on Systems, Man, and Cybernetics
Publisher
IEEE
Year
2011

Abstract

Automated systems are increasingly complex, making it hard to design interfaces for human operators. Human-machine interaction (HMI) errors like automation surprises are more likely to appear and lead to system failures or accidents. In previous work, we studied the problem of generating system abstractions, called mental models, that facilitate system understanding while allowing proper control of the system by operators as defined by the full-control property. Both the domain and its mental model have Labelled Transition Systems (LTS) semantics, and we proposed algorithms for automatically generating minimal mental models as well as checking full-control.

This paper presents a methodology and an associated framework for using the above and other formal method based algorithms to support the design of HMI systems. The framework can be used for modelling HMI systems and analysing models against HMI vulnerabilities. The analysis can be used for validation purposes or for generating artifacts such as mental models, manuals and recovery procedures. The framework is implemented in the JavaPathfinder model checker. Our methodology is demonstrated on two examples, an existing benchmark of a medical device, and a model generated from the ADEPT toolset developed at NASA Ames. Guidelines about how ADEPT models can be translated automatically into JavaPathfinder models are also discussed.

Tags Tags: , , , , ,

BibTeX Record
  @INPROCEEDINGS{lvl-2011-3,
    TITLE = {A Formal Framework for Design and Analysis of Human-Machine Interaction},
    AUTHOR = {Sébastien Combéfis and Dimitra Giannakopoulou and Charles Pecheur and Michael Feary},
    YEAR = {2011},
    PUBLISHER = {IEEE},
    URL = {https://lvl.info.ucl.ac.be/Publications/AFormalFrameworkForDesignAndAnalysisOfHuman-MachineInteraction},
  }