State Event Models for the Formal Analysis of Human-Machine Interactions
(2014) AAAI 2014 Symposium “Modeling in Human Machine Systems: Challenges for Formal Verification” — Location: Palo Alto, 2014 (24.March.2014)
Files
combefis-fvhms2014.pdf
Restricted Access - Adobe PDF
- 460.47 KB
Details
- Authors
- Abstract
- The work described in this paper was motivated by our experience with applying a framework for formal analysis 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 simple, full-control, mental models for their human operators. For this reason, our framework supports automated generation of minimal full-control mental models for HMI systems, where both the system and the mental models are described as labelled transition systems (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.
- Affiliations
Citations
Combéfis, S., Giannakopoulou, D., & Pecheur, C. (2014). State Event Models for the Formal Analysis of Human-Machine Interactions. AAAI 2014 Symposium “Modeling in Human Machine Systems: Challenges for Formal Verification”, Palo Alto, 2014. https://hdl.handle.net/2078.5/231725