{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T04:37:17Z","timestamp":1781239037357,"version":"3.54.1"},"publisher-location":"Cham","reference-count":48,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319518374","type":"print"},{"value":"9783319518381","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-51838-1_13","type":"book-chapter","created":{"date-parts":[[2017,4,24]],"date-time":"2017-04-24T08:23:43Z","timestamp":1493022223000},"page":"343-377","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["Enhanced Operator Function Model (EOFM): A Task Analytic Modeling Formalism for Including Human Behavior in the Verification of Complex Systems"],"prefix":"10.1007","author":[{"given":"Matthew L.","family":"Bolton","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ellen J.","family":"Bass","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2017,4,25]]},"reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"Abbate AJ, Throckmorton AL, Bass EJ (2016) A formal task analytic approach to medical device alarm troubleshooting instructions. IEEE Trans Hum-Mach Syst 46(1):53\u201365","DOI":"10.1109\/THMS.2015.2494462"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"A\u00eft-Ameur Y, Baron M (2006) Formal and experimental validation approaches in HCI systems design based on a shared event B model. Int J Softw Tools Technol Transf 8(6):547\u2013563","DOI":"10.1007\/s10009-006-0008-8"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"Angluin D (1987) Learning regular sets from queries and counterexamples. Inf Comput 75(2):87\u2013106","DOI":"10.1016\/0890-5401(87)90052-6"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"Basnyat S, Palanque P, Schupp B, Wright P (2007) Formal socio-technical barrier modelling for safety-critical interactive systems design. Saf Sci 45(5):545\u2013565","DOI":"10.1016\/j.ssci.2007.01.001"},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"Bass EJ, Bolton ML, Feigh K, Griffith D, Gunter E, Mansky W, Rushby J (2011) Toward a multi-method approach to formalizing human-automation interaction and human-human communications. In: Proceedings of the IEEE international conference on systems, man, and cybernetics. IEEE, Piscataway, pp 1817\u20131824","DOI":"10.1109\/ICSMC.2011.6083935"},{"key":"13_CR6","unstructured":"Bogdanich W (2010) The radiation boom: radiation offers new cures, and ways to do harm. New York Times 23:23\u201327"},{"key":"13_CR7","unstructured":"Bolton ML, Bass EJ (2011) Using task analytic behavior models, strategic knowledge-based erroneous human behavior generation, and model checking to evaluate human-automation interaction. In: Proceedings of the IEEE international conference on systems man and cybernetics. IEEE, Piscataway, pp 1788\u20131794"},{"key":"13_CR8","unstructured":"Bolton ML (2011) Validating human-device interfaces with model checking and temporal logic properties automatically generated from task analytic models. In: Proceedings of the 20th behavior representation in modeling and simulation conference. The BRIMS Society, Sundance, pp 130\u2013137"},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"Bolton ML (2013) Automatic validation and failure diagnosis of human-device interfaces using task analytic models and model checking. Comput Math Organ Theory 19(3):288\u2013312","DOI":"10.1007\/s10588-012-9138-6"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"Bolton ML (2015) Model checking human-human communication protocols using task models and miscommunication generation. J Aerosp Inf Syst 12:476\u2013489","DOI":"10.2514\/1.I010276"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Bolton ML, Bass EJ (2010a) Formally verifying human-automation interaction as part of a system model: limitations and tradeoffs. Innov Syst Softw Eng: A NASA J 6(3):219\u2013231","DOI":"10.1007\/s11334-010-0129-9"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"Bolton ML, Bass EJ (2010b) Using task analytic models and phenotypes of erroneous human behavior to discover system failures using model checking. In: Proceedings of the human factors and ergonomics society annual meeting. HFES, Santa Monica, pp 992\u2013996","DOI":"10.1177\/154193121005401315"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Bolton ML, Bass EJ (2010c) Using task analytic models to visualize model checker counterexamples. In: Proceedings of the 2010 IEEE international conference on systems, man, and cybernetics. IEEE, Piscataway, pp 2069\u20132074","DOI":"10.1109\/ICSMC.2010.5641711"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"Bolton ML, Bass EJ (2012) Using model checking to explore checklist-guided pilot behavior. Int J Aviat Psychol 22:343\u2013366","DOI":"10.1080\/10508414.2012.718240"},{"key":"13_CR15","unstructured":"Bolton ML, Bass EJ (2013) Generating erroneous human behavior from strategic knowledge in task models and evaluating its impact on system safety with model checking. IEEE Trans Syst Man Cybern: Syst 43(6):1314\u20131327"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"Bolton ML, Siminiceanu RI, Bass EJ (2011) A systematic approach to model checking human-automation interaction using task-analytic models. IEEE Trans Syst Man Cybern Part A 41(5):961\u2013976","DOI":"10.1109\/TSMCA.2011.2109709"},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"Bolton ML, Bass EJ, Siminiceanu RI (2012) Using phenotypical erroneous human behavior generation to evaluate human-automation interaction using model checking. Int J Hum-Comput Stud 70:888\u2013906","DOI":"10.1016\/j.ijhcs.2012.05.010"},{"key":"13_CR18","doi-asserted-by":"crossref","unstructured":"Bolton ML, Bass EJ, Siminiceanu RI (2013) Using formal verification to evaluate human-automation interaction: a review. IEEE Trans Syst Man Cybern: Syst 43(3):488\u2013503","DOI":"10.1109\/TSMCA.2012.2210406"},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"Bolton ML, Jimenez N, van Paassen MM, Trujillo M (2014) Automatically generating specification properties from task models for the formal verification of human-automation interaction. IEEE Trans Hum-Mach Syst 44(5):561\u2013575","DOI":"10.1109\/THMS.2014.2329476"},{"key":"13_CR20","doi-asserted-by":"publisher","unstructured":"Bolton ML, Zheng X, Molinaro K, Houser A, Li M (2016) Improving the scalability of formal human-automation interaction verification analyses that use task analytic models. Innov Syst Softw Eng: A NASA J (in press). doi: 10.1007\/s11334-016-0272-z","DOI":"10.1007\/s11334-016-0272-z"},{"key":"13_CR21","unstructured":"Clark J, Murata M (2001) Relax NG specification. Committee Specification. http:\/\/relaxng.org\/spec-20011203.html"},{"key":"13_CR22","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura L, Owre S, Shankar N (2003) The SAL language manual. Technical Report CSL-01-01, Computer Science Laboratory, SRI International, Menlo Park. http:\/\/staffwww.dcs.shef.ac.uk\/people\/A.Simons\/z2sal\/saldocs\/SALlanguage.pdf","DOI":"10.1007\/978-3-540-27813-9_45"},{"key":"13_CR23","doi-asserted-by":"crossref","unstructured":"Degani A, Heymann M, Shafto M (1999) Formal aspects of procedures: the problem of sequential correctness. Proceedings of the 43rd annual meeting of the human factors and ergonomics society. HFES, Santa Monica, pp 1113\u20131117","DOI":"10.1177\/154193129904302012"},{"key":"13_CR24","unstructured":"Fields RE (2001) Analysis of erroneous actions in the design of critical systems. PhD thesis, University of York, York"},{"key":"13_CR25","doi-asserted-by":"crossref","unstructured":"Giese M, Mistrzyk T, Pfau A, Szwillus G, von Detten M (2008) AMBOSS: a task modeling approach for safety-critical systems. In: Proceedings of the second international conference on human-centered software engineering. Springer, Berlin, pp 98\u2013109","DOI":"10.1007\/978-3-540-85992-5_8"},{"key":"13_CR26","unstructured":"Gunter EL, Yasmeen A, Gunter CA, Nguyen A (2009) Specifying and analyzing workflows for automated identification and data capture. In: Proceedings of the 42nd Hawaii international conference on system sciences. IEEE Computer Society, Los Alamitos, pp 1\u201311"},{"key":"13_CR27","doi-asserted-by":"crossref","unstructured":"Hartson HR, Siochi AC, Hix D (1990) The UAN: a user-oriented representation for direct manipulation interface designs. ACM Trans Inf Syst 8(3):181\u2013203","DOI":"10.1145\/98188.98191"},{"key":"13_CR28","doi-asserted-by":"crossref","unstructured":"Hollnagel E (1993) The phenotype of erroneous actions. Int J Man-Mach Stud 39(1):1\u201332","DOI":"10.1006\/imms.1993.1051"},{"key":"13_CR29","doi-asserted-by":"crossref","unstructured":"Kirwan B, Ainsworth LK (1992) A guide to task analysis. Taylor and Francis, London","DOI":"10.1201\/b16826"},{"key":"13_CR30","unstructured":"Le H\u00e9garet P (2002) The w3c document object model (DOM). http:\/\/www.w3.org\/2002\/07\/26-dom-article.html"},{"key":"13_CR31","unstructured":"Leveson NG, Turner CS (1993) An investigation of the therac-25 accidents. Computer 26(7):18\u201341"},{"key":"13_CR32","doi-asserted-by":"crossref","unstructured":"Li M, Molinaro K, Bolton ML (2015) Learning formal human-machine interface designs from task analytic models. In: Proceedings of the HFES annual meeting. HFES, Santa Monica, pp 652\u2013656","DOI":"10.1177\/1541931215591142"},{"key":"13_CR33","doi-asserted-by":"crossref","unstructured":"Martinie C, Palanque P, Barboni E, Ragosta M (2011) Task-model based assessment of automation levels: application to space ground segments. In: Proceedings of the 2011 IEEE international conference on systems, man, and cybernetics. Piscataway, IEEE, pp 3267\u20133273","DOI":"10.1109\/ICSMC.2011.6084173"},{"key":"13_CR34","doi-asserted-by":"crossref","unstructured":"Martinie C, Navarre D, Palanque P (2014) A multi-formalism approach for model-based dynamic distribution of user interfaces of critical interactive systems. Int J Hum-Comput Stud 72(1):77\u201399","DOI":"10.1016\/j.ijhcs.2013.08.013"},{"key":"13_CR35","unstructured":"Mitchell CM, Miller RA (1986) A discrete control model of operator function: a methodology for information display design. IEEE Trans Syst Man Cybern Part A: Syst Hum 16(3):343\u2013357"},{"key":"13_CR36","unstructured":"NTSB (2001) Runway Overrun During Landing, American Airlines Flight 1420, McDonnell Douglas MD-82, N215AA, Little Rock, Arkansas, June 1, 1999 Technical Report NTSB\/AAR-01\/02. National Transportation Safety Board, Washington, DC"},{"key":"13_CR37","unstructured":"NTSB (2015) Runway Overrun During Rejected Takeoff Gulfstream Aerospace Corporation G-IV, N121JM, Bedford, Massachusetts, May 31, 2014 Technical Report NTSB\/AAR-15\/03. National Transportation Safety Board, Washington, DC"},{"key":"13_CR38","doi-asserted-by":"crossref","unstructured":"Palanque PA, Bastide R, Senges V (1996) Validating interactive system design through the verification of formal task and system models. In: Proceedings of the IFIP TC2\/WG2.7 working conference on engineering for human-computer interaction. Chapman and Hall Ltd., London, pp 189\u2013212","DOI":"10.1007\/978-0-387-34907-7_11"},{"key":"13_CR39","doi-asserted-by":"crossref","unstructured":"Pan D, Bolton ML (2015) A formal method for evaluating the performance level of human-human collaborative procedures. In: Proceedings of HCI international. Springer, Berlin, pp 186\u2013197","DOI":"10.1007\/978-3-319-20907-4_17"},{"key":"13_CR40","doi-asserted-by":"publisher","unstructured":"Pan D, Bolton ML (2016) Properties for formally assessing the performance level of human-human collaborative procedures with miscommunications and erroneous human behavior. Int J Ind Ergon (in press). doi: 10.1016\/j.ergon.2016.04.001","DOI":"10.1016\/j.ergon.2016.04.001"},{"key":"13_CR41","doi-asserted-by":"crossref","unstructured":"Patern\u00f2 F, Santoro C (2001) Integrating model checking and HCI tools to help designers verify user interface properties. In: Proceedings of the 7th international workshop on the design, specification, and verification of interactive systems. Springer, Berlin, pp 135\u2013150","DOI":"10.1007\/3-540-44675-3_9"},{"key":"13_CR42","doi-asserted-by":"crossref","unstructured":"Patern\u00f2 F, Mancini C, Meniconi S (1997) Concurtasktrees: a diagrammatic notation for specifying task models. In: Proceedings of the IFIP TC13 international conference on human-computer interaction. Chapman and Hall Ltd, London, pp 362\u2013369","DOI":"10.1007\/978-0-387-35175-9_58"},{"key":"13_CR43","doi-asserted-by":"crossref","unstructured":"Perrow C (1999) Normal accidents: living with high-risk technologies. Princeton University Press, Princeton","DOI":"10.1515\/9781400828494"},{"key":"13_CR44","doi-asserted-by":"crossref","unstructured":"Reason J (1990) Human error. Cambridge University Press, New York","DOI":"10.1017\/CBO9781139062367"},{"key":"13_CR45","doi-asserted-by":"crossref","unstructured":"Shankar N (2000) Symbolic analysis of transition systems. Proceedings of the international workshop on abstract state machines, theory and applications. Springer, London, pp 287\u2013302","DOI":"10.1007\/3-540-44518-8_16"},{"key":"13_CR46","unstructured":"Sheridan TB, Parasuraman R (2005) Human-automation interaction. Rev Hum Factors Ergon 1(1):89\u2013129"},{"key":"13_CR47","unstructured":"Syncro Soft (2016) Relax NG schema diagram. In: User Manual of Oxygen XML Editor 17.1. https:\/\/www.oxygenxml.com\/doc\/versions\/17.1\/ug-editor\/index.html#topics\/relax-ng-schema-diagram.html"},{"key":"13_CR48","doi-asserted-by":"crossref","unstructured":"van Paassen MM, Bolton ML, Jimenez N (2014) Checking formal verification models for human-automation interaction. 2014 IEEE international conference on systems, man and cybernetics (SMC). IEEE, Piscataway, pp 3709\u20133714","DOI":"10.1109\/SMC.2014.6974507"}],"updated-by":[{"DOI":"10.1007\/978-3-319-51838-1_21","type":"erratum","label":"Erratum","source":"publisher","updated":{"date-parts":[[2017,7,29]],"date-time":"2017-07-29T00:00:00Z","timestamp":1501286400000}}],"container-title":["Human\u2013Computer Interaction Series","The Handbook of Formal Methods in Human-Computer Interaction"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-51838-1_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,6]],"date-time":"2020-10-06T04:06:59Z","timestamp":1601957219000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-51838-1_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319518374","9783319518381"],"references-count":48,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-51838-1_13","relation":{"erratum":[{"id-type":"doi","id":"10.1007\/978-3-319-51838-1_21","asserted-by":"object"}]},"ISSN":["1571-5035"],"issn-type":[{"value":"1571-5035","type":"print"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"25 April 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}