Formal Analysis of Human Behaviour in Interactive Systems

Experiments with simulators allow psychologists to better understand the causes of human errors and build models of cognitive processes. In previous work, in cooperation with the University of Queensland, Australia, with inputs from Airservices Australia, a cognitive model for an air traffic control system simulator has been formalised using the CSP process algebra and automatically verified using model-checking. The automatic verification has shown the existence of behavioural patterns which had been overlooked by the psychologists in their analysis and has contributed to improve the cognitive model.

This project aims to define a generic formal model for goal-based tasks to be applied to case studies such as the above mentioned air traffic control system. The model will be analysed at two different levels:

• a high level where the cognitive model is specified in a process algebra language and the patterns of behaviour are expressed as temporal logic properties and are analysed both qualitatively and quantitatively using model-checking techniques;
• a low level where single actions of a hci process are specified and organised in the appropriate sequence to achieve a given task while model-checking is used to verify the absence of specific errors, such as post-completion errors.