An Executable Formal Framework for Safety-Critical Human Multitasking

  • Giovanna BrocciaEmail author
  • Paolo Milazzo
  • Peter Csaba Ölveczky
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10811)


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).


  1. 1.
    Arrington, C.M., Logan, G.D.: Voluntary task switching: chasing the elusive homunculus. J. Exp. Psychol. Learn. Mem. Cogn. 31(4), 683–702 (2005)CrossRefGoogle Scholar
  2. 2.
    Australian Transport Safety Bureau: Dangerous distraction. Safety Investigation Report B2004/0324 (2005)Google Scholar
  3. 3.
    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)CrossRefGoogle Scholar
  4. 4.
    Broccia, G., Milazzo, P., Ölveczky, P.: An executable formal framework for safety-critical human multitasking (2017). Report:
  5. 5.
    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). CrossRefGoogle Scholar
  6. 6.
    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)CrossRefGoogle Scholar
  7. 7.
    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). Google Scholar
  8. 8.
    Clark, T., et al.: Impact of clinical alarms on patient safety. Technical report, ACCE Healthcare Technology Foundation (2006)Google Scholar
  9. 9.
    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). zbMATHGoogle Scholar
  10. 10.
    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)CrossRefGoogle Scholar
  11. 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
  12. 12.
    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)CrossRefGoogle Scholar
  13. 13.
    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)CrossRefGoogle Scholar
  14. 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
  15. 15.
    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)CrossRefGoogle Scholar
  16. 16.
    Lofsky, A.S.: Turn your alarms on! APSF Newsl.: Off. J. Anesth. Patient Saf. Found. 19(4), 43 (2005)Google Scholar
  17. 17.
    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)CrossRefGoogle Scholar
  18. 18.
    Ölveczky, P.C.: Real-Time Maude and its applications. In: Escobar, S. (ed.) WRLA 2014. LNCS, vol. 8663, pp. 42–79. Springer, Cham (2014). Google Scholar
  19. 19.
    Ölveczky, P.C., Meseguer, J.: Semantics and pragmatics of Real-Time Maude. High.-Order Symb. Comput. 20(1–2), 161–196 (2007)CrossRefzbMATHGoogle Scholar
  20. 20.
    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)CrossRefzbMATHGoogle Scholar
  21. 21.
    Salvucci, D.D., Taatgen, N.A.: Threaded cognition: an integrated theory of concurrent multitasking. Psychol. Rev. 115(1), 101–130 (2008)CrossRefGoogle Scholar
  22. 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
  23. 23.
    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)CrossRefGoogle Scholar
  24. 24.
    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)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.Department of Computer ScienceUniversity of PisaPisaItaly
  2. 2.University of OsloOsloNorway

Personalised recommendations