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.