{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,9]],"date-time":"2024-07-09T13:59:17Z","timestamp":1720533557454},"reference-count":49,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2019,4,8]],"date-time":"2019-04-08T00:00:00Z","timestamp":1554681600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2019,4,8]],"date-time":"2019-04-08T00:00:00Z","timestamp":1554681600000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100007514","name":"Universit\u00e0 di Pisa","doi-asserted-by":"publisher","award":["PRA 2017_44"],"id":[{"id":"10.13039\/501100007514","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2019,9]]},"DOI":"10.1007\/s11334-019-00333-7","type":"journal-article","created":{"date-parts":[[2019,4,8]],"date-time":"2019-04-08T16:35:47Z","timestamp":1554741347000},"page":"169-190","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["Formal modeling and analysis of safety-critical human multitasking"],"prefix":"10.1007","volume":"15","author":[{"given":"Giovanna","family":"Broccia","sequence":"first","affiliation":[]},{"ORCID":"http:\/\/orcid.org\/0000-0002-7309-6424","authenticated-orcid":false,"given":"Paolo","family":"Milazzo","sequence":"additional","affiliation":[]},{"given":"Peter Csaba","family":"\u00d6lveczky","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,4,8]]},"reference":[{"key":"333_CR1","unstructured":"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\u2013278"},{"key":"333_CR2","doi-asserted-by":"crossref","unstructured":"AlTurki M, Meseguer J (2011) PVeStA: a parallel statistical model checking and quantitative analysis tool. In: CALCO\u201911, LNCS, vol 6859. Springer","DOI":"10.1007\/978-3-642-22944-2_28"},{"issue":"4","key":"333_CR3","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1207\/s15327051hci1204_5","volume":"12","author":"JR Anderson","year":"1997","unstructured":"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\u2013462","journal-title":"Hum Comput Interact"},{"issue":"4","key":"333_CR4","doi-asserted-by":"publisher","first-page":"683","DOI":"10.1037\/0278-7393.31.4.683","volume":"31","author":"CM Arrington","year":"2005","unstructured":"Arrington CM, Logan GD (2005) Voluntary task switching: chasing the elusive homunculus. J Exp Psychol Learn Mem Cogn 31(4):683\u2013702","journal-title":"J Exp Psychol Learn Mem Cogn"},{"key":"333_CR5","first-page":"89","volume-title":"Psychology of learning and motivation","author":"RC Atkinson","year":"1968","unstructured":"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\u2013195"},{"key":"333_CR6","unstructured":"Australian Transport Safety Bureau: Dangerous distraction. Safety Investigation Report B2004\/0324 (2005)"},{"key":"333_CR7","doi-asserted-by":"crossref","unstructured":"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\u201912. ACM, pp 1651\u20131654","DOI":"10.1145\/2207676.2208289"},{"issue":"1","key":"333_CR8","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1037\/0096-3445.133.1.83","volume":"133","author":"P Barrouillet","year":"2004","unstructured":"Barrouillet P, Bernardin S, Camos V (2004) Time constraints and resource sharing in adults\u2019 working memory spans. J Exp Psychol Gen 133(1):83\u2013100","journal-title":"J Exp Psychol Gen"},{"issue":"3","key":"333_CR9","doi-asserted-by":"publisher","first-page":"570","DOI":"10.1037\/0278-7393.33.3.570","volume":"33","author":"P Barrouillet","year":"2007","unstructured":"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):570","journal-title":"J Exp Psychol Learn Mem Cogn"},{"issue":"1","key":"333_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/jmla.2001.2767","volume":"45","author":"P Barrouillet","year":"2001","unstructured":"Barrouillet P, Camos V (2001) Developmental increase in working memory span: resource sharing or temporal decay? J Mem Lang 45(1):1\u201320","journal-title":"J Mem Lang"},{"issue":"2","key":"333_CR11","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1037\/a0014615","volume":"45","author":"P Barrouillet","year":"2009","unstructured":"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):477","journal-title":"Dev Psychol"},{"key":"333_CR12","unstructured":"Broccia G (2019) A formal framework for modelling and analysing safety-critical human multitasking. Ph.D. thesis, University of Pisa (in preparation)"},{"key":"333_CR13","doi-asserted-by":"crossref","unstructured":"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\u20139:7","DOI":"10.1145\/3220134.3220140"},{"key":"333_CR14","doi-asserted-by":"crossref","unstructured":"Broccia G, Milazzo P, \u00d6lveczky PC (2018) An executable formal framework for safety-critical human multitasking. In: NASA formal methods (NFM 2018), LNCS, vol 10811. Springer","DOI":"10.1007\/978-3-319-77935-5_4"},{"key":"333_CR15","doi-asserted-by":"crossref","unstructured":"Broccia G, Milazzo P, \u00d6lveczky PC (2018) An algorithm for simulating human selective attention. In: SEFM 2017 collocated workshops, LNCS, vol 10729. Springer","DOI":"10.1007\/978-3-319-74781-1_4"},{"issue":"1\u20133","key":"333_CR16","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1016\/j.tcs.2006.04.012","volume":"360","author":"R Bruni","year":"2006","unstructured":"Bruni R, Meseguer J (2006) Semantic foundations for generalized rewrite theories. Theor Comput Sci 360(1\u20133):386\u2013414","journal-title":"Theor Comput Sci"},{"issue":"2","key":"333_CR17","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1207\/s15327108ijap1502_2","volume":"15","author":"MD Byrne","year":"2005","unstructured":"Byrne MD, Kirlik A (2005) Using computational cognitive modeling to diagnose possible sources of aviation error. Int J Aviat Psychol 15(2):135\u2013155","journal-title":"Int J Aviat Psychol"},{"key":"333_CR18","doi-asserted-by":"crossref","unstructured":"Cerone A (2016) A cognitive framework based on rewriting logic for the analysis of interactive systems. In: SEFM 2016, LNCS, vol 9763. Springer","DOI":"10.1007\/978-3-319-41591-8_20"},{"issue":"4","key":"333_CR19","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/j.ijhcs.2007.09.001","volume":"66","author":"PH Chung","year":"2008","unstructured":"Chung PH, Byrne MD (2008) Cue effectiveness in mitigating postcompletion errors in a routine procedural task. Int J Hum Comput Stud 66(4):217\u2013232","journal-title":"Int J Hum Comput Stud"},{"key":"333_CR20","unstructured":"Clark T et al (2006) Impact of clinical alarms on patient safety. Technical report, ACCE Healthcare Technology Foundation"},{"key":"333_CR21","unstructured":"Clavel M, Dur\u00e1n F, Eker S, Lincoln P, Mart\u00ed-Oliet N, Meseguer J, Talcott C (2007) All About Maude, LNCS, vol 4350. Springer"},{"issue":"10","key":"333_CR22","doi-asserted-by":"publisher","first-page":"2636","DOI":"10.1073\/pnas.1513271113","volume":"113","author":"TA Dingus","year":"2016","unstructured":"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\u20132641","journal-title":"Proc Natl Acad Sci"},{"key":"333_CR23","doi-asserted-by":"crossref","unstructured":"Dismukes R, Nowinski J (2007) Prospective memory, concurrent task management, and pilot error. In: Attention: from theory to practice. Oxford University Press","DOI":"10.1093\/acprof:oso\/9780195305722.003.0016"},{"issue":"5509","key":"333_CR24","doi-asserted-by":"publisher","first-page":"1803","DOI":"10.1126\/science.1056496","volume":"291","author":"JW de Fockert","year":"2001","unstructured":"de Fockert JW, Rees G, Frith CD, Lavie N (2001) The role of working memory in visual selective attention. Science 291(5509):1803\u20131806","journal-title":"Science"},{"issue":"5","key":"333_CR25","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1109\/THMS.2014.2331034","volume":"44","author":"G Gelman","year":"2014","unstructured":"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\u2013590","journal-title":"IEEE Trans Hum Mach Syst"},{"key":"333_CR26","doi-asserted-by":"crossref","unstructured":"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\u20136","DOI":"10.1109\/ComplexSys.2015.7385975"},{"issue":"1","key":"333_CR27","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s11334-017-0305-2","volume":"14","author":"A Houser","year":"2018","unstructured":"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\u201314","journal-title":"Innov Syst Softw Eng"},{"key":"333_CR28","doi-asserted-by":"crossref","unstructured":"Iqbal ST, Bailey BP (2005) Investigating the effectiveness of mental workload as a predictor of opportune moments for interruption. In: CHI\u201905 extended abstracts on Human factors in computing systems. ACM","DOI":"10.1145\/1056808.1056948"},{"key":"333_CR29","doi-asserted-by":"crossref","unstructured":"Joshi A, Miller SP, Heimdahl MPE (2003) Mode confusion analysis of a flight guidance system using formal methods. In: Digital avionics systems conference (DASC\u201903). IEEE","DOI":"10.1109\/DASC.2003.1245813"},{"issue":"2","key":"333_CR30","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1109\/THMS.2015.2509980","volume":"46","author":"J Krall","year":"2016","unstructured":"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\u2013230","journal-title":"IEEE Trans Hum Mach Syst"},{"key":"333_CR31","doi-asserted-by":"crossref","unstructured":"Lepri D, \u00c1brah\u00e1m E, \u00d6lveczky PC (2013) A timed CTL model checker for Real-Time Maude. In: CALCO\u201913, LNCS, vol 8089. Springer","DOI":"10.1007\/978-3-642-40206-7_27"},{"key":"333_CR32","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1016\/j.scico.2014.06.006","volume":"99","author":"D Lepri","year":"2015","unstructured":"Lepri D, \u00c1brah\u00e1m E, \u00d6lveczky PC (2015) Sound and complete timed CTL model checking of timed Kripke structures and real-time rewrite theories. Sci Comput Program 99:128\u2013192","journal-title":"Sci Comput Program"},{"issue":"4","key":"333_CR33","first-page":"43","volume":"19","author":"AS Lofsky","year":"2005","unstructured":"Lofsky AS (2005) Turn your alarms on!. APSF Newslett 19(4):43","journal-title":"APSF Newslett"},{"key":"333_CR34","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J Meseguer","year":"1992","unstructured":"Meseguer J (1992) Conditional rewriting logic as a unified model of concurrency. Theor Comput Sci 96:73\u2013155","journal-title":"Theor Comput Sci"},{"key":"333_CR35","doi-asserted-by":"crossref","unstructured":"Meseguer J (1998) Membership algebra as a logical framework for equational specification. In: Proceedings of the WADT\u201997, LNCS, vol 1376. Springer","DOI":"10.1007\/3-540-64299-4_26"},{"issue":"2","key":"333_CR36","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1037\/h0043158","volume":"63","author":"GA Miller","year":"1956","unstructured":"Miller GA (1956) The magical number seven, plus or minus two: some limits on our capacity for processing information. Psychol Rev 63(2):81\u201397","journal-title":"Psychol Rev"},{"key":"333_CR37","volume-title":"Plans and the structure of behavior","author":"GA Miller","year":"1986","unstructured":"Miller GA, Galanter E, Pribram KH (1986) Plans and the structure of behavior. Adams Bannister Cox, New York"},{"key":"333_CR38","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky PC (2014) Real-Time Maude and its applications. In: WRLA 2014, LNCS, vol 8663. Springer (2014)","DOI":"10.1007\/978-3-319-12904-4_3"},{"key":"333_CR39","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1016\/S0304-3975(01)00363-2","volume":"285","author":"PC \u00d6lveczky","year":"2002","unstructured":"\u00d6lveczky PC, Meseguer J (2002) Specification of real-time and hybrid systems in rewriting logic. Theor Comput Sci 285:359\u2013405","journal-title":"Theor Comput Sci"},{"issue":"1\u20132","key":"333_CR40","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/s10990-007-9001-5","volume":"20","author":"PC \u00d6lveczky","year":"2007","unstructured":"\u00d6lveczky PC, Meseguer J (2007) Semantics and pragmatics of Real-Time Maude. High Order Symb Comput 20(1\u20132):161\u2013196","journal-title":"High Order Symb Comput"},{"issue":"1","key":"333_CR41","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1006\/ijhc.2001.0472","volume":"55","author":"DD Salvucci","year":"2001","unstructured":"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\u2013107","journal-title":"Int J Hum Comput Stud"},{"issue":"1","key":"333_CR42","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1037\/0033-295X.115.1.101","volume":"115","author":"DD Salvucci","year":"2008","unstructured":"Salvucci DD, Taatgen NA (2008) Threaded cognition: an integrated theory of concurrent multitasking. Psychol Rev 115(1):101\u2013130","journal-title":"Psychol Rev"},{"key":"333_CR43","unstructured":"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\u2019s guide. NASA tech. rep."},{"issue":"8","key":"333_CR44","doi-asserted-by":"publisher","first-page":"571","DOI":"10.1016\/j.ssci.2005.04.001","volume":"43","author":"ST Shorrock","year":"2005","unstructured":"Shorrock ST (2005) Errors of memory in air traffic control. Saf Sci 43(8):571\u2013588","journal-title":"Saf Sci"},{"key":"333_CR45","unstructured":"Todd BK, Fischer J, Falgout J, Schweers J (2013) Basic operational robotics instructional system. NASA tech. rep."},{"key":"333_CR46","unstructured":"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\u00a061. SAGE Publications, pp 757\u2013761"},{"key":"333_CR47","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/j.ijhcs.2015.01.002","volume":"79","author":"CD Wickens","year":"2015","unstructured":"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\u201384","journal-title":"Int J Hum Comput Stud"},{"issue":"2","key":"333_CR48","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1177\/0018720815622761","volume":"58","author":"CD Wickens","year":"2016","unstructured":"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\u2013343","journal-title":"Hum Factors"},{"issue":"6","key":"333_CR49","doi-asserted-by":"publisher","first-page":"959","DOI":"10.1177\/0018720814566454","volume":"57","author":"CD Wickens","year":"2015","unstructured":"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\u2013975","journal-title":"Hum Factors"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-019-00333-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11334-019-00333-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-019-00333-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,14]],"date-time":"2020-05-14T16:45:44Z","timestamp":1589474744000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11334-019-00333-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,4,8]]},"references-count":49,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2019,9]]}},"alternative-id":["333"],"URL":"https:\/\/doi.org\/10.1007\/s11334-019-00333-7","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,4,8]]},"assertion":[{"value":"1 October 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 March 2019","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 April 2019","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}