A Formal Framework for the Analysis of Human-Machine Interactions

There are more and more automated systems with which people are led to interact everyday. Their increasing complexity makes it harder for operators to drive them safely, in particular because badly designed systems may result in automation surprises. Several accidents are due to such surprising situations, as testified by real accidents. Examples include the Three Mile Island nuclear meltdown, the lethal radiation doses administered by the Therac 25 medical device, or the shot down of the aircraft of the KAL007 flight.
The contribution of this thesis is a formal analysis framework to assess whether a system is prone to potential automation surprises in an interaction. Potential automation surprises are captured by the full-control property. The minimal fullcontrol conceptual model generation problem consists in finding a minimal conceptual model that allows full-control of the system. The existence of such conceptual model is characterised by the fc-deterministic property.
The generated models can be used to generate artifacts, such as user manuals. Three algorithms are proposed : the first one uses three-valued deterministic finite automata that characterise the fullcontrol property in terms of traces ; the second one uses a variant of the Paige-Tarjan reduction algorithm, and the third one uses the L active learning algorithm. The proposed framework has been tested on various examples, among which a large case study of an autopilot coming from ADEPT, a toolset to support designers in the early design phases of automation interfaces.
Experiences show that the method proposed in this thesis can identify existing automation surprises and also find new ones.