• cognitive science
• formal analysis
• human-computer interaction
• model checking
• modelling
• safety-critical system
• simulation
• verification

Nowadays people often interact with multiple devices or with a single device performing multiple tasks. In such a multitasking context, the amount of cognitive resources required from each task (cognitive load) influences the activity of the attentional mechanisms of the user. In particular, focusing attention on a “main” task (e.g. driving a car) may be impeded by a secondary “distractor” task (e.g. using a GPS navigator system) with a high cognitive load. Moreover, the cognitive resource that is mostly involved in interactions with computers and other technological devices is the human working memory, which is a volatile memory with a limited capacity used to store and process the information necessary for performing a task. The concurrent use of such a resource might cause memory overloading
and might get the users to forget useful information for the interaction with one of the systems. When human multitasking involves safety-critical tasks, failure to devote sufficient attention to some tasks (the safety-critical ones) could have serious consequences.
To study these kinds of problem we define a formal model of safety-critical human multitasking which describes the cognitive processes involved in HCI and the switching of attention among concurrent tasks. The model describes the attention attractiveness of each task as a factor proportional to the task cognitive load, its criticality and the time it was ignored during the interaction. The model builds on classical results from applied psychology on selective attention and working memory.
We implement the model through a simulator, which allows us to get quick feedback about whether a human can safely perform multiple such tasks at the same time, and as an executable formal framework in Real-Time Maude, which enables us to analyse safety-critical human multitasking through simulation and reachability analysis.
We validate the model against data collected from an experimental study with real users involved in the interaction with two concurrent tasks.
We show how a number of prototypical multitasking problems can be analysed in Real-Time Maude by studying: (i) the interaction with a GPS navigation system while driving, (ii) a medical operator setting multiple infusion pumps simultaneously, and (iii) some typical scenarios involving human errors in air traffic control.