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
 combefis-smc2011.pdf Δ   312Kb   12 Sep 2011
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 = {http://lvl.info.ucl.ac.be/Publications/AFormalFrameworkForDesignAndAnalysisOfHuman-MachineInteraction},
  }