Publications

A JavaPathfinder Extension to Analyse Human-Machine Interactions

Authors
Sébastien Combéfis, Dimitra Giannakopoulou, Charles Pecheur, Peter Mehlitz
Tags
, , ,
Title
A JavaPathfinder Extension to Analyse Human-Machine Interactions
Authors
Sébastien Combéfis, Dimitra Giannakopoulou, Charles Pecheur, Peter Mehlitz
combefis-jpfworkshop2011.pdf Δ   234Kb   28 May 2020
Type
In Proceedings
Book title
Java Pathfinder Workshop 2011
Year
2011

Abstract

We present jpf-hmi, a Java Pathfinder (JPF) extension that supports the description and analysis of human machine interaction (HMI) systems. The extension is built on top of jpf-statechart, but differentiates between events in terms of commands, observations and internal actions, as it is typical in the HMI domain. jpf-hmi implements two algorithms for generating concise system models for human operators. It also supports the detection of several types of HMI-specific anomalies known as "automation surprises", such as non full-control determinism and mode confusion. These capabilities are provided in addition to the existing more generic property verification that is supported by JPF, and which can also be applied to HMI systems.

Tags Tags: , , ,


BibTeX Record
  @INPROCEEDINGS{lvl-2011-959764,
    TITLE = {A JavaPathfinder Extension to Analyse Human-Machine Interactions},
    AUTHOR = {Sébastien Combéfis and Dimitra Giannakopoulou and Charles Pecheur and Peter Mehlitz},
    YEAR = {2011},
    URL = {https://lvl.info.ucl.ac.be/Publications/AJavaPathfinderExtensionToAnalyseHuman-MachineInteractions},
  }