Formal modeling and analysis of safety-critical human multitasking

  • Giovanna Broccia
  • Paolo MilazzoEmail author
  • Peter Csaba Ölveczky
S.I. : NFM2018


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.


Human–computer interaction Safety-critical systems Human multitasking Cognitive models Real-Time Maude Model checking 



We thank Paolo Masci for his contributions to the infusion pump case study and the anonymous reviewers for their very helpful comments on an earlier version of this paper.


  1. 1.
    Adamczyk PD, Bailey BP (2004) If not now, when? The effects of interruption at different moments within task execution. In: Proceedings of the SIGCHI conference on human factors in computing systems. ACM, pp 271–278Google Scholar
  2. 2.
    AlTurki M, Meseguer J (2011) PVeStA: a parallel statistical model checking and quantitative analysis tool. In: CALCO’11, LNCS, vol 6859. SpringerGoogle Scholar
  3. 3.
    Anderson JR, Matessa M, Lebiere C (1997) ACT-R: a theory of higher level cognition and its relation to visual attention. Hum Comput Interact 12(4):439–462CrossRefGoogle Scholar
  4. 4.
    Arrington CM, Logan GD (2005) Voluntary task switching: chasing the elusive homunculus. J Exp Psychol Learn Mem Cogn 31(4):683–702CrossRefGoogle Scholar
  5. 5.
    Atkinson RC, Shiffrin RM (1968) Human memory: a proposed system and its control processes. In: Spence KW, Spence JT (eds) Psychology of learning and motivation, vol 2. Academic Press, London, pp 89–195Google Scholar
  6. 6.
    Australian Transport Safety Bureau: Dangerous distraction. Safety Investigation Report B2004/0324 (2005)Google Scholar
  7. 7.
    Back J, Cox A, Brumby D (2012) Choosing to interleave: human error and information access cost. In: SIGCHI conference on human factors in computing systems, CHI’12. ACM, pp 1651–1654Google Scholar
  8. 8.
    Barrouillet P, Bernardin S, Camos V (2004) Time constraints and resource sharing in adults’ working memory spans. J Exp Psychol Gen 133(1):83–100CrossRefGoogle Scholar
  9. 9.
    Barrouillet P, Bernardin S, Portrat S, Vergauwe E, Camos V (2007) Time and cognitive load in working memory. J Exp Psychol Learn Mem Cogn 33(3):570CrossRefGoogle Scholar
  10. 10.
    Barrouillet P, Camos V (2001) Developmental increase in working memory span: resource sharing or temporal decay? J Mem Lang 45(1):1–20CrossRefGoogle Scholar
  11. 11.
    Barrouillet P, Gavens N, Vergauwe E, Gaillard V, Camos V (2009) Working memory span development: a time-based resource-sharing model account. Dev Psychol 45(2):477CrossRefGoogle Scholar
  12. 12.
    Broccia G (2019) A formal framework for modelling and analysing safety-critical human multitasking. Ph.D. thesis, University of Pisa (in preparation)Google Scholar
  13. 13.
    Broccia G, Masci P, Milazzo P (2018) Modeling and analysis of human memory load in multitasking scenarios. In: Proceedings of the SIGCHI symposium on engineering interactive computing systems (EICS 2018). ACM, pp 9:1–9:7Google Scholar
  14. 14.
    Broccia G, Milazzo P, Ölveczky PC (2018) An executable formal framework for safety-critical human multitasking. In: NASA formal methods (NFM 2018), LNCS, vol 10811. SpringerGoogle Scholar
  15. 15.
    Broccia G, Milazzo P, Ölveczky PC (2018) An algorithm for simulating human selective attention. In: SEFM 2017 collocated workshops, LNCS, vol 10729. SpringerGoogle Scholar
  16. 16.
    Bruni R, Meseguer J (2006) Semantic foundations for generalized rewrite theories. Theor Comput Sci 360(1–3):386–414MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Byrne MD, Kirlik A (2005) Using computational cognitive modeling to diagnose possible sources of aviation error. Int J Aviat Psychol 15(2):135–155CrossRefGoogle Scholar
  18. 18.
    Cerone A (2016) A cognitive framework based on rewriting logic for the analysis of interactive systems. In: SEFM 2016, LNCS, vol 9763. SpringerGoogle Scholar
  19. 19.
    Chung PH, Byrne MD (2008) Cue effectiveness in mitigating postcompletion errors in a routine procedural task. Int J Hum Comput Stud 66(4):217–232CrossRefGoogle Scholar
  20. 20.
    Clark T et al (2006) Impact of clinical alarms on patient safety. Technical report, ACCE Healthcare Technology FoundationGoogle Scholar
  21. 21.
    Clavel M, Durán F, Eker S, Lincoln P, Martí-Oliet N, Meseguer J, Talcott C (2007) All About Maude, LNCS, vol 4350. SpringerGoogle Scholar
  22. 22.
    Dingus TA, Guo F, Lee S, Antin JF, Perez M, Buchanan-King M, Hankey J (2016) Driver crash risk factors and prevalence evaluation using naturalistic driving data. Proc Natl Acad Sci 113(10):2636–2641CrossRefGoogle Scholar
  23. 23.
    Dismukes R, Nowinski J (2007) Prospective memory, concurrent task management, and pilot error. In: Attention: from theory to practice. Oxford University PressGoogle Scholar
  24. 24.
    de Fockert JW, Rees G, Frith CD, Lavie N (2001) The role of working memory in visual selective attention. Science 291(5509):1803–1806CrossRefGoogle Scholar
  25. 25.
    Gelman G, Feigh KM, Rushby JM (2014) Example of a complementary use of model checking and human performance simulation. IEEE Trans Hum Mach Syst 44(5):576–590CrossRefGoogle Scholar
  26. 26.
    Houser A, Ma LM, Feigh K, Bolton ML (2015) A formal approach to modeling and analyzing human taskload in simulated air traffic scenarios. In: Complex systems engineering (ICCSE). IEEE, pp 1–6Google Scholar
  27. 27.
    Houser A, Ma LM, Feigh KM, Bolton ML (2018) Using formal methods to reason about taskload and resource conflicts in simulated air traffic scenarios. Innov Syst Softw Eng 14(1):1–14CrossRefGoogle Scholar
  28. 28.
    Iqbal ST, Bailey BP (2005) Investigating the effectiveness of mental workload as a predictor of opportune moments for interruption. In: CHI’05 extended abstracts on Human factors in computing systems. ACMGoogle Scholar
  29. 29.
    Joshi A, Miller SP, Heimdahl MPE (2003) Mode confusion analysis of a flight guidance system using formal methods. In: Digital avionics systems conference (DASC’03). IEEEGoogle Scholar
  30. 30.
    Krall J, Menzies T, Davies M (2016) Learning mitigations for pilot issues when landing aircraft (via multiobjective optimization and multiagent simulations). IEEE Trans Hum Mach Syst 46(2):221–230CrossRefGoogle Scholar
  31. 31.
    Lepri D, Ábrahám E, Ölveczky PC (2013) A timed CTL model checker for Real-Time Maude. In: CALCO’13, LNCS, vol 8089. SpringerGoogle Scholar
  32. 32.
    Lepri D, Ábrahám E, Ölveczky PC (2015) Sound and complete timed CTL model checking of timed Kripke structures and real-time rewrite theories. Sci Comput Program 99:128–192CrossRefGoogle Scholar
  33. 33.
    Lofsky AS (2005) Turn your alarms on!. APSF Newslett 19(4):43Google Scholar
  34. 34.
    Meseguer J (1992) Conditional rewriting logic as a unified model of concurrency. Theor Comput Sci 96:73–155MathSciNetCrossRefzbMATHGoogle Scholar
  35. 35.
    Meseguer J (1998) Membership algebra as a logical framework for equational specification. In: Proceedings of the WADT’97, LNCS, vol 1376. SpringerGoogle Scholar
  36. 36.
    Miller GA (1956) The magical number seven, plus or minus two: some limits on our capacity for processing information. Psychol Rev 63(2):81–97CrossRefGoogle Scholar
  37. 37.
    Miller GA, Galanter E, Pribram KH (1986) Plans and the structure of behavior. Adams Bannister Cox, New YorkGoogle Scholar
  38. 38.
    Ölveczky PC (2014) Real-Time Maude and its applications. In: WRLA 2014, LNCS, vol 8663. Springer (2014)Google Scholar
  39. 39.
    Ölveczky PC, Meseguer J (2002) Specification of real-time and hybrid systems in rewriting logic. Theor Comput Sci 285:359–405MathSciNetCrossRefzbMATHGoogle Scholar
  40. 40.
    Ölveczky PC, Meseguer J (2007) Semantics and pragmatics of Real-Time Maude. High Order Symb Comput 20(1–2):161–196CrossRefzbMATHGoogle Scholar
  41. 41.
    Salvucci DD (2001) Predicting the effects of in-car interface use on driver performance: an integrated model approach. Int J Hum Comput Stud 55(1):85–107CrossRefzbMATHGoogle Scholar
  42. 42.
    Salvucci DD, Taatgen NA (2008) Threaded cognition: an integrated theory of concurrent multitasking. Psychol Rev 115(1):101–130CrossRefGoogle Scholar
  43. 43.
    Santiago-Espada Y, Myer RR, Latorella KA, Comstock JR Jr (2011) The multi-attribute task battery II (MATB-II) software for human performance and workload research: a user’s guide. NASA tech. rep.Google Scholar
  44. 44.
    Shorrock ST (2005) Errors of memory in air traffic control. Saf Sci 43(8):571–588CrossRefGoogle Scholar
  45. 45.
    Todd BK, Fischer J, Falgout J, Schweers J (2013) Basic operational robotics instructional system. NASA tech. rep.Google Scholar
  46. 46.
    Wickens CD, Gutzwiller RS (2017) The status of the strategic task overload model (STOM) for predicting multi-task management. In: Proceedings of the human factors and ergonomics society annual meeting, vol 61. SAGE Publications, pp 757–761Google Scholar
  47. 47.
    Wickens CD, Gutzwiller RS, Santamaria A (2015) Discrete task switching in overload: a meta-analyses and a model. Int J Hum Comput Stud 79:79–84CrossRefGoogle Scholar
  48. 48.
    Wickens CD, Gutzwiller RS, Vieane A, Clegg BA, Sebok A, Janes J (2016) Time sharing between robotics and process control: validating a model of attention switching. Hum Factors 58(2):322–343CrossRefGoogle Scholar
  49. 49.
    Wickens CD, Sebok A, Li H, Sarter N, Gacy AM (2015) Using modeling and simulation to predict operator performance and automation-induced complacency with robotic automation: a case study and empirical validation. Hum Factors 57(6):959–975CrossRefGoogle Scholar

Copyright information

© Springer-Verlag London Ltd., part of Springer Nature 2019

Authors and Affiliations

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

Personalised recommendations