A JavaPathfinder Extension to Analyse Human-Machine Interactions
(2011) The Java Pathfinder Workshop 2011 — Location: Oread, Lawrence, Kansas (12.November.2011)
Files
combefis-jpfworkshop2011.pdf
Restricted Access - Adobe PDF
- 169.75 KB
Details
- Authors
- 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.
- Affiliations
NASA Ames Research Center Moffett Field, USA
Citations
Combéfis, S., Giannakopoulou, D., Pecheur, C., & Mehlitz, P. (2011). A JavaPathfinder Extension to Analyse Human-Machine Interactions. The Java Pathfinder Workshop 2011, Oread, Lawrence, Kansas. https://hdl.handle.net/2078.5/226636