State Event Models for the Formal Analysis of Human-Machine Interactions

The work described in this paper was motivated by our experience with applying a framework for formal anal-ysis of human-machine interactions (HMI) to a realistic model of an autopilot. The framework is built around a formally defined conformance relation called “full-control ” between an actual system and the mental model according to which the system is operated. Systems are well-designed if they can be described by relatively sim-ple, full-control, mental models for their human oper-ators. For this reason, our framework supports auto-mated generation of minimal full-control mental mod-els for HMI systems, where both the system and the mental models are described as labelled transition sys-tems (LTS). The autopilot that we analysed has been developed in the NASA Ames HMI prototyping tool ADEPT. In this paper, we describe how we extended the models that our HMI analysis framework handles to allow adequate representation of ADEPT models. We then provide a property-preserving reduction from these extended models to LTSs, to enable application of our LTS-based formal analysis algorithms. Finally, we briefly discuss the analyses we were able to perform on the autopilot model with our extended framework