An Executable Formal Framework for Safety-Critical Human Multitasking

2/21/2018

By Giovanna Broccia, University of Pisa, Italy.

Abstract. 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 flying an airplane, driving a car, or using medical devices, failure to devote sufficient attention to the different tasks could have serious consequences. 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 proto- typical multitasking problems can be analyzed in Real-Time Maude..

Keywords. Software engineering, Formal modeling, Human multitasking, Safety-critical systems, Model checking, Real-Time Maude.

About the Speaker. Giovanna is a PhD Student in Computer Science at the University of Pisa and member of the research group “Modelling, Simulation and Verification of Biological System”. Although she obtained her Bachelor Degree on European Literature for Publishing and Cultural Production and the Masters Degree on Digital Humanities, Giovanna’s interests currently lie in the field of modelling and verification of cognitive systems, Human-Computer Interaction, and usage of formal methods in different application domains. Her PhD thesis is on the creation of an executable formal model to analyze safety-critical human multitasking through simulation, reachability analysis, and model checking. Giovanna has already published several international publications in reputable venues in her area.