A JavaPathfinder Extension to Analyse Human-Machine Interactions

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.