Formal Framework for Detection of Automation Surprises in Human-machine Systems Modeled by Hybrid Automata

Consumer products are human-machine systems, and a design of a user interface is an important issue. A user identifies the behaviors of the machine using partial or abstracted information provided by the user interface, and gives a command. If the information is not sufficient for his/her operation, its response to the operation may be different from his/her expected one. Such a situation is called an automation surprise, which leads to an erroneous operation. In this paper, we consider the machine modeled by a hybrid system and a user model including temporal information. The user interface is modeled by a binary relation between the machine model and the user model. Thus, a formal model of the human-machine system is given by a hybrid automaton. We define three types of automation surprises and show conditions for the nonexistence of the automation surprises.