NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
State Event Models for the Formal Analysis of Human-Machine InteractionsThe 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 "fullcontrol" 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.
Document ID
20150002694
Acquisition Source
Ames Research Center
Document Type
Conference Paper
Authors
Combefis, Sebastien
(Universite Catholique de Louvain Belgium)
Giannakopoulou, Dimitra
(NASA Ames Research Center Moffett Field, CA, United States)
Pecheur, Charles
(Universite Catholique de Louvain Belgium)
Date Acquired
March 10, 2015
Publication Date
March 24, 2014
Subject Category
Computer Programming And Software
Report/Patent Number
ARC-E-DAA-TN13396
Report Number: ARC-E-DAA-TN13396
Meeting Information
Meeting: Association for the Advancement of Artificial Intelligence (AAAI) 2014 Symposium
Location: Palo Alto, CA
Country: United States
Start Date: March 24, 2014
End Date: March 26, 2014
Sponsors: Association for the Advancement of Artificial Intelligence
Funding Number(s)
WBS: WBS 534723.02.02.01.40
Distribution Limits
Public
Copyright
Public Use Permitted.
Keywords
State-event Models
Human-machine Interactions
Formal Analysis
No Preview Available