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, 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 is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Since we now consider structured tasks and add delays to basic tasks, we redefine the cognitive load of a task to be \(\sum \frac{d_i t_i}{t_i + dly _i}\), where \(d_i\), \(t_i\) and \( dly _i\) denote the difficulty, duration and delay of each basic task i of the current subtask. The cognitive load of a task therefore changes every time a new subtask begins, and remains the same throughout the execution of the subtask.
- 2.
We do not show the variable declarations, but follow the convention that variables are written in all capital letters.
- 3.
The variable A:AttributeSet captures the other attributes in inner objects.
References
Arrington, C.M., Logan, G.D.: Voluntary task switching: chasing the elusive homunculus. J. Exp. Psychol. Learn. Mem. Cogn. 31(4), 683–702 (2005)
Australian Transport Safety Bureau: Dangerous distraction. Safety Investigation Report B2004/0324 (2005)
Barrouillet, P., Bernardin, S., Camos, V.: Time constraints and resource sharing in adults’ working memory spans. J. Exp. Psychol. Gen. 133(1), 83–100 (2004)
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
Broccia, G., Milazzo, P., Ölveczky, P.C.: An algorithm for simulating human selective attention. In: Cerone, A., Roveri, M. (eds.) SEFM 2017. LNCS, vol. 10729, pp. 48–55. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-74781-1_4
Byrne, M.D., Kirlik, A.: Using computational cognitive modeling to diagnose possible sources of aviation error. Int. J. Aviat. Psychol. 15(2), 135–155 (2005)
Cerone, A.: A cognitive framework based on rewriting logic for the analysis of interactive systems. In: De Nicola, R., Kühn, E. (eds.) SEFM 2016. LNCS, vol. 9763, pp. 287–303. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41591-8_20
Clark, T., et al.: Impact of clinical alarms on patient safety. Technical report, ACCE Healthcare Technology Foundation (2006)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71999-1
Dingus, T.A., Guo, F., Lee, S., Antin, J.F., Perez, M., Buchanan-King, M., Hankey, J.: Driver crash risk factors and prevalence evaluation using naturalistic driving data. Proc. Nat. Acad. Sci. 113(10), 2636–2641 (2016)
Dismukes, R., Nowinski, J.: Prospective memory, concurrent task management, and pilot error. In: Attention: From Theory to Practice. Oxford University Press, Oxford (2007)
de Fockert, J.W., Rees, G., Frith, C.D., Lavie, N.: The role of working memory in visual selective attention. Science 291(5509), 1803–1806 (2001)
Gelman, G., Feigh, K.M., Rushby, J.M.: Example of a complementary use of model checking and human performance simulation. IEEE Trans. Hum.-Mach. Syst. 44(5), 576–590 (2014)
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)
Lepri, D., Ábrahám, E., Ölveczky, P.C.: Sound and complete timed CTL model checking of timed Kripke structures and real-time rewrite theories. Sci. Comput. Program. 99, 128–192 (2015)
Lofsky, A.S.: Turn your alarms on! APSF Newsl.: Off. J. Anesth. Patient Saf. Found. 19(4), 43 (2005)
Miller, G.A.: The magical number seven, plus or minus two: some limits on our capacity for processing information. Psychol. Rev. 63(2), 81–97 (1956)
Ölveczky, P.C.: Real-Time Maude and its applications. In: Escobar, S. (ed.) WRLA 2014. LNCS, vol. 8663, pp. 42–79. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-12904-4_3
Ölveczky, P.C., Meseguer, J.: Semantics and pragmatics of Real-Time Maude. High.-Order Symb. Comput. 20(1–2), 161–196 (2007)
Salvucci, D.D.: Predicting the effects of in-car interface use on driver performance: an integrated model approach. Int. J. Hum. Comput. Stud. 55(1), 85–107 (2001)
Salvucci, D.D., Taatgen, N.A.: Threaded cognition: an integrated theory of concurrent multitasking. Psychol. Rev. 115(1), 101–130 (2008)
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)
Wickens, C.D., Sebok, A., Li, H., Sarter, N., Gacy, A.M.: Using modeling and simulation to predict operator performance and automation-induced complacency with robotic automation: a case study and empirical validation. Hum. Fact. 57(6), 959–975 (2015)
Wickens, C.D., Gutzwiller, R.S., Vieane, A., Clegg, B.A., Sebok, A., Janes, J.: Time sharing between robotics and process control: validating a model of attention switching. Hum. Fact. 58(2), 322–343 (2016)
Acknowledgments
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).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this paper
Cite this paper
Broccia, G., Milazzo, P., Ölveczky, P.C. (2018). An Executable Formal Framework for Safety-Critical Human Multitasking. In: Dutle, A., Muñoz, C., Narkawicz, A. (eds) NASA Formal Methods. NFM 2018. Lecture Notes in Computer Science(), vol 10811. Springer, Cham. https://doi.org/10.1007/978-3-319-77935-5_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-77935-5_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-77934-8
Online ISBN: 978-3-319-77935-5
eBook Packages: Computer ScienceComputer Science (R0)