{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T12:08:53Z","timestamp":1725970133098},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319779348"},{"type":"electronic","value":"9783319779355"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-77935-5_4","type":"book-chapter","created":{"date-parts":[[2018,3,10]],"date-time":"2018-03-10T10:02:34Z","timestamp":1520676154000},"page":"54-69","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["An Executable Formal Framework for Safety-Critical Human Multitasking"],"prefix":"10.1007","author":[{"ORCID":"http:\/\/orcid.org\/0000-0002-4737-5761","authenticated-orcid":false,"given":"Giovanna","family":"Broccia","sequence":"first","affiliation":[]},{"given":"Paolo","family":"Milazzo","sequence":"additional","affiliation":[]},{"given":"Peter Csaba","family":"\u00d6lveczky","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,3,11]]},"reference":[{"issue":"4","key":"4_CR1","doi-asserted-by":"crossref","first-page":"683","DOI":"10.1037\/0278-7393.31.4.683","volume":"31","author":"CM Arrington","year":"2005","unstructured":"Arrington, C.M., Logan, G.D.: Voluntary task switching: chasing the elusive homunculus. J. Exp. Psychol. Learn. Mem. Cogn. 31(4), 683\u2013702 (2005)","journal-title":"J. Exp. Psychol. Learn. Mem. Cogn."},{"key":"4_CR2","unstructured":"Australian Transport Safety Bureau: Dangerous distraction. Safety Investigation Report B2004\/0324 (2005)"},{"issue":"1","key":"4_CR3","doi-asserted-by":"crossref","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.: Time constraints and resource sharing in adults\u2019 working memory spans. J. Exp. Psychol. Gen. 133(1), 83\u2013100 (2004)","journal-title":"J. Exp. Psychol. Gen."},{"key":"4_CR4","unstructured":"Broccia, G., Milazzo, P., \u00d6lveczky, P.: An executable formal framework for safety-critical human multitasking (2017). Report: http:\/\/www.di.unipi.it\/msvbio\/software\/HumanMultitasking.html"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-319-74781-1_4","volume-title":"Software Engineering and Formal Methods","author":"G Broccia","year":"2018","unstructured":"Broccia, G., Milazzo, P., \u00d6lveczky, P.C.: An algorithm for simulating human selective attention. In: Cerone, A., Roveri, M. (eds.) SEFM 2017. LNCS, vol. 10729, pp. 48\u201355. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-74781-1_4"},{"issue":"2","key":"4_CR6","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1207\/s15327108ijap1502_2","volume":"15","author":"MD Byrne","year":"2005","unstructured":"Byrne, M.D., Kirlik, A.: Using computational cognitive modeling to diagnose possible sources of aviation error. Int. J. Aviat. Psychol. 15(2), 135\u2013155 (2005)","journal-title":"Int. J. Aviat. Psychol."},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-319-41591-8_20","volume-title":"Software Engineering and Formal Methods","author":"A Cerone","year":"2016","unstructured":"Cerone, A.: A cognitive framework based on rewriting logic for the analysis of interactive systems. In: De Nicola, R., K\u00fchn, E. (eds.) SEFM 2016. LNCS, vol. 9763, pp. 287\u2013303. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41591-8_20"},{"key":"4_CR8","unstructured":"Clark, T., et al.: Impact of clinical alarms on patient safety. Technical report, ACCE Healthcare Technology Foundation (2006)"},{"key":"4_CR9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71999-1","volume-title":"All About Maude - A High-Performance Logical Framework","author":"M Clavel","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-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"},{"issue":"10","key":"4_CR10","doi-asserted-by":"crossref","first-page":"2636","DOI":"10.1073\/pnas.1513271113","volume":"113","author":"TA Dingus","year":"2016","unstructured":"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\u20132641 (2016)","journal-title":"Proc. Nat. Acad. Sci."},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Dismukes, R., Nowinski, J.: Prospective memory, concurrent task management, and pilot error. In: Attention: From Theory to Practice. Oxford University Press, Oxford (2007)","DOI":"10.1093\/acprof:oso\/9780195305722.003.0016"},{"issue":"5509","key":"4_CR12","doi-asserted-by":"crossref","first-page":"1803","DOI":"10.1126\/science.1056496","volume":"291","author":"JW Fockert de","year":"2001","unstructured":"de Fockert, J.W., Rees, G., Frith, C.D., Lavie, N.: The role of working memory in visual selective attention. Science 291(5509), 1803\u20131806 (2001)","journal-title":"Science"},{"issue":"5","key":"4_CR13","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1109\/THMS.2014.2331034","volume":"44","author":"G Gelman","year":"2014","unstructured":"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\u2013590 (2014)","journal-title":"IEEE Trans. Hum.-Mach. Syst."},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1109\/DASC.2003.1245813"},{"key":"4_CR15","doi-asserted-by":"crossref","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, P.C.: Sound and complete timed CTL model checking of timed Kripke structures and real-time rewrite theories. Sci. Comput. Program. 99, 128\u2013192 (2015)","journal-title":"Sci. Comput. Program."},{"key":"4_CR16","unstructured":"Lofsky, A.S.: Turn your alarms on! APSF Newsl.: Off. J. Anesth. Patient Saf. Found. 19(4), 43 (2005)"},{"issue":"2","key":"4_CR17","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1037\/h0043158","volume":"63","author":"GA Miller","year":"1956","unstructured":"Miller, G.A.: The magical number seven, plus or minus two: some limits on our capacity for processing information. Psychol. Rev. 63(2), 81\u201397 (1956)","journal-title":"Psychol. Rev."},{"key":"4_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-319-12904-4_3","volume-title":"Rewriting Logic and Its Applications","author":"PC \u00d6lveczky","year":"2014","unstructured":"\u00d6lveczky, P.C.: Real-Time Maude and its applications. In: Escobar, S. (ed.) WRLA 2014. LNCS, vol. 8663, pp. 42\u201379. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-12904-4_3"},{"issue":"1\u20132","key":"4_CR19","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1007\/s10990-007-9001-5","volume":"20","author":"PC \u00d6lveczky","year":"2007","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: Semantics and pragmatics of Real-Time Maude. High.-Order Symb. Comput. 20(1\u20132), 161\u2013196 (2007)","journal-title":"High.-Order Symb. Comput."},{"issue":"1","key":"4_CR20","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1006\/ijhc.2001.0472","volume":"55","author":"DD Salvucci","year":"2001","unstructured":"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\u2013107 (2001)","journal-title":"Int. J. Hum. Comput. Stud."},{"issue":"1","key":"4_CR21","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1037\/0033-295X.115.1.101","volume":"115","author":"DD Salvucci","year":"2008","unstructured":"Salvucci, D.D., Taatgen, N.A.: Threaded cognition: an integrated theory of concurrent multitasking. Psychol. Rev. 115(1), 101\u2013130 (2008)","journal-title":"Psychol. Rev."},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"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\u2013761. SAGE Publications (2017)","DOI":"10.1177\/1541931213601674"},{"issue":"6","key":"4_CR23","doi-asserted-by":"crossref","first-page":"959","DOI":"10.1177\/0018720814566454","volume":"57","author":"CD Wickens","year":"2015","unstructured":"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\u2013975 (2015)","journal-title":"Hum. Fact."},{"issue":"2","key":"4_CR24","doi-asserted-by":"crossref","first-page":"322","DOI":"10.1177\/0018720815622761","volume":"58","author":"CD Wickens","year":"2016","unstructured":"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\u2013343 (2016)","journal-title":"Hum. Fact."}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-77935-5_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,12]],"date-time":"2019-10-12T13:01:44Z","timestamp":1570885304000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-77935-5_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319779348","9783319779355"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-77935-5_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}