Checking Human Machine Interactions

by Sébastien Combéfis for The Java Pathfinder Team

The goal of the project is to robustify the jpf-hmi extension that has been started last year. Such extension allows to check human-machine interaction, by analysing system and mental models, modelled with LTSs encoded as JPF-statecharts. The HMI analysis is based on a full-control property. The project aims at integrating the ADEPT toolset developed at NASA Ames.