An Executable Formal Framework for 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, for example in an airplane, a spacecraft, or a car, 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 prototypical multitasking problems can be analyzed in Real-Time Maude. We illustrate our modeling and analysis framework by studying the interaction with a GPS navigation system while driving, and 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.
This work has been supported by the project “Metodologie informatiche avanzate per l’analisi di dati biomedici” funded by the University of Pisa (PRA 2017 44).
- 2.Australian Transport Safety Bureau: Dangerous distraction. Safety Investigation Report B2004/0324 (2005)Google Scholar
- 4.Broccia, G., Milazzo, P., Ölveczky, P.: An executable formal framework for safety-critical human multitasking (2017). Report: http://www.di.unipi.it/msvbio/software/HumanMultitasking.html
- 8.Clark, T., et al.: Impact of clinical alarms on patient safety. Technical report, ACCE Healthcare Technology Foundation (2006)Google Scholar
- 11.Dismukes, R., Nowinski, J.: Prospective memory, concurrent task management, and pilot error. In: Attention: From Theory to Practice. Oxford University Press, Oxford (2007)Google Scholar
- 14.Joshi, A., Miller, S.P., Heimdahl, M.P.E.: Mode confusion analysis of a flight guidance system using formal methods. In: Digital Avionics Systems Conference (DASC 2003). IEEE (2003)Google Scholar
- 16.Lofsky, A.S.: Turn your alarms on! APSF Newsl.: Off. J. Anesth. Patient Saf. Found. 19(4), 43 (2005)Google Scholar
- 22.Wickens, C.D., Gutzwiller, R.S.: The status of the strategic task overload model (STOM) for predicting multi-task management. In: Proceedings of Human Factors and Ergonomics Society Annual Meeting, vol. 61, pp. 757–761. SAGE Publications (2017)Google Scholar