Formal modeling and analysis of safety-critical human multitasking

When a person is concurrently interacting with different systems, the amount of cognitive resources required (cognitive load) could be too high and might prevent some tasks from being completed. When such human multitasking involves safety-critical tasks, such as in an airplane, a spacecraft, or a car, failure to devote sufficient attention to the different tasks could have serious consequences. For example, using a GPS with high cognitive load while driving might take the attention away for too long from the safety-critical task of driving the car. To study this problem, we define an executable formal model of human attention and multitasking in Real-Time Maude. It includes a description of the human working memory and the cognitive processes involved in the interaction with a device. Our framework enables us to analyze human multitasking through simulation, reachability analysis, and LTL and timed CTL model checking, and we show how a number of prototypical multitasking problems can be analyzed in Real-Time Maude. We illustrate our modeling and analysis framework by studying: (i) the interaction with a GPS navigation system while driving, (ii) some typical scenarios involving human errors in air traffic control (ATC), and (iii) a medical operator setting multiple infusion pumps simultaneously. We apply model checking to show that in some cases the cognitive load of the navigation system could cause the driver to keep the focus away from driving for too long, and that working memory overload and distraction may cause an air traffic controller or a medical operator to make critical mistakes.