A Formal Framework for Modelling and Analysing Safety-Critical Human Multitasking

This thesis is focused on the creation of a formal model of a multitasking interaction with safety-critical systems. The model describes the cognitive processes involved in human-computer interaction and the switching of attention among concurrent tasks, and it builds on classical results from applied psychology on selective attention and working memory.

The model has been implemented through a Java Simulator, which can be used to have a quick feedback on whether users can safely complete multiple tasks at the same time.

Afterward, the model has been implemented through a computational model in Real-Time Maude, which enables us to analyse multitasking through simulation and reachability analysis.

We validate the algorithm underlying the model, against data gathered from an experimental study we devised in collaboration with a group of psychologists of the University of Pisa. We implemented a web application where users were asked to interact with two concurrent tasks.

Finally, we show how a number of prototypical multitasking problems can be analysed in Real-Time Maude by applying our framework to three case studies.