{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,30]],"date-time":"2025-12-30T23:34:58Z","timestamp":1767137698970,"version":"build-2238731810"},"publisher-location":"Cham","reference-count":40,"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":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-51838-1_15","type":"book-chapter","created":{"date-parts":[[2017,4,24]],"date-time":"2017-04-24T04:23:43Z","timestamp":1493007823000},"page":"405-431","source":"Crossref","is-referenced-by-count":0,"title":["Formal Analysis of Multiple Coordinated HMI Systems"],"prefix":"10.1007","author":[{"given":"Guillaume","family":"Brat","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S\u00e9bastien","family":"Comb\u00e9fis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dimitra","family":"Giannakopoulou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Charles","family":"Pecheur","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Franco","family":"Raimondi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Neha","family":"Rungta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,4,25]]},"reference":[{"key":"15_CR1","doi-asserted-by":"publisher","unstructured":"Ameur YA, Boniol F, Wiels V (2010) Toward a wider use of formal methods for aerospace systems design and verification. Int J Softw Tools Technol Transf 12(1):1\u20137. ISSN 1433-2779. doi: 10.1007\/s10009-009-0131-4","DOI":"10.1007\/s10009-009-0131-4"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Bastide R, Navarre D, Palanque P (2003) A tool-supported design framework for safety critical interactive systems. Interact Comput 15(3):309\u2013328","DOI":"10.1016\/S0953-5438(03)00011-0"},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"Bolton M, Siminiceanu R, Bass E (2011) A systematic approach to model checking human-automation interaction using task analytic models. IEEE Trans Syst Man Cybern Part A: Syst Hum 41(5):961\u2013976","DOI":"10.1109\/TSMCA.2011.2109709"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Bolton M, Bass E (2010) Using task analytic models and phenotypes of erroneous human behavior to discover system failures using model checking. In: Proceedings of the 54th annual meeting of the human factors and ergonomics society, pp 992\u2013996","DOI":"10.1177\/154193121005401315"},{"key":"15_CR5","unstructured":"Bolton M, Bass E, Siminiceanu R (2008) Using formal methods to predict human error and system failures. In: Proceedings of the second international conference on applied human factors and ergonomics (AHFE 2008)"},{"key":"15_CR6","unstructured":"Bovair Susan, Kieras DE, Polson PG (1990) The acquisition and performance of text-editing skill: a cognitive complexity analysis. Hum Comput Interact 5(1):1\u201348"},{"key":"15_CR7","unstructured":"Bratman M (1987) Intention, plans, and practical reason"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"Bredereke J, Lankenau A (2002) A rigorous view of mode confusion. In: Proceedings of the 21st international conference on computer safety, reliability and security (SAFECOMP 2002). Springer, pp 19\u201331, Sept 2002","DOI":"10.1007\/3-540-45732-1_4"},{"key":"15_CR9","doi-asserted-by":"crossref","unstructured":"Bredereke J, Lankenau A (2005) Safety-relevant mode confusions\u2013modelling and reducing them. Reliab Eng Syst Saf 88(3):229\u2013245","DOI":"10.1016\/j.ress.2004.07.020"},{"key":"15_CR10","unstructured":"Butterworth R, Blandford A (1997) Programmable user models: the story so far. Middlesex University, London"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"Campos JC, Harrison MD (2008) Systematic analysis of control panel interfaces using formal tools. In: Nicholas Graham TC, Palanque PA (eds) Proceedings of the 15th international workshop on design, specification and verification of interactive systems (DSV-IS 2008), vol 5136. Springer, Lecture notes in computer science, pp 72\u201385","DOI":"10.1007\/978-3-540-70569-7_6"},{"key":"15_CR12","unstructured":"Campos JC, Harrison MD (2011) Model checking interactor specifications. Autom Softw Eng 8(3):275\u2013310"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Clancey WJ, Sachs P, Sierhuis M, Van Hoof R (1998) Brahms: simulating practice for work systems design. Int J Hum Comput Stud 49(6):831\u2013865","DOI":"10.1006\/ijhc.1998.0229"},{"key":"15_CR14","unstructured":"Comb\u00e9fis S (2009) Operational model: integrating user tasks and environment information with system model. In: Proceedings of the 3rd international workshop on formal methods for interactive systems, pp 83\u201386"},{"key":"15_CR15","unstructured":"Comb\u00e9fis S (2013) A formal framework for the analysis of human-machine interactions. PhD thesis, Universit\u00e9 catholique de Louvain"},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"Comb\u00e9fis S, Giannakopoulou D, Pecheur C (2016) Automatic detection of potential automation surprises for ADEPT models. IEEE Trans Hum Mach Syst Spec Issue Syst Approaches Hum Mach Interface Improv Resil Robust Stab 46(2):","DOI":"10.1109\/THMS.2015.2424851"},{"key":"15_CR17","doi-asserted-by":"publisher","unstructured":"Comb\u00e9fis S, Giannakopoulou D, Pecheur C, Feary M (2011) A formal framework for design and analysis of human-machine interaction. In: Proceedings of the IEEE international conference on systems, man and cybernetics, Anchorage, Alaska, USA, 9\u201312 Oct 2011. IEEE, pp 1801\u20131808. ISBN 978-1-4577-0652-3. doi: 10.1109\/ICSMC.2011.6083933","DOI":"10.1109\/ICSMC.2011.6083933"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"Comb\u00e9fis S, Pecheur C (2009) A bisimulation-based approach to the analysis of human-computer interaction. In: Calvary G, Nicholas Graham TC, Gray P (eds) Proceedings of the ACM SIGCHI symposium on engineering interactive computing systems (EICS\u201909)","DOI":"10.1145\/1570433.1570454"},{"key":"15_CR19","doi-asserted-by":"crossref","unstructured":"Curzon P, Ruk\u0161\u0117nas R, Blandford A (2007) An approach to formal verification of human-computer interaction. Formal Aspects Comput 19(4):513\u2013550","DOI":"10.1007\/s00165-007-0035-6"},{"key":"15_CR20","unstructured":"Feary MS (2010) A toolset for supporting iterative human\u2014automation interaction in design. Technical Report 20100012861, NASA Ames Research Center, March 2010"},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"Godefroid P (1997) Model checking for programming languages using verisoft. In: Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on principles of programming languages. ACM, pp 174\u2013186","DOI":"10.1145\/263699.263717"},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"Heymann M, Degani A (2007) Formal analysis and automatic generation of user interfaces: approach, methodology, and an algorithm. Hum Factors: J Hum Factors Ergon Soc 49(2):311\u2013330","DOI":"10.1518\/001872007X312522"},{"key":"15_CR23","unstructured":"Hunter J, Raimondi F, Rungta N, Stocker R (2013) A synergistic and extensible framework for multi-agent system verification. In: Proceedings of the 2013 international conference on autonomous agents and multi-agent systems. International Foundation for Autonomous Agents and Multiagent Systems, pp 869\u2013876"},{"key":"15_CR24","unstructured":"JavaPathfinder (JPF) (2016). http:\/\/babelfish.arc.nasa.gov\/trac\/jpf\/"},{"key":"15_CR25","doi-asserted-by":"crossref","unstructured":"Javaux D (2002) A method for predicting errors when interacting with finite state systems. How implicit learning shapes the user\u2019s knowledge of a system. Reliab Eng Syst Saf 75:147\u2013165","DOI":"10.1016\/S0951-8320(01)00091-6"},{"key":"15_CR26","doi-asserted-by":"crossref","unstructured":"Johnson J, Henderson A (2002) Conceptual models: begin by designing what to design. Interactions 9:25\u201332","DOI":"10.1145\/503355.503366"},{"key":"15_CR27","doi-asserted-by":"crossref","unstructured":"Lee PU, Smith NM, Homola J, Brasil C, Buckley N, Cabrall C, Chevalley E, Parke B, Yoo HS (2015) Reducing departure delays at laguardia airport with departure-sensitive arrival spacing (dsas) operations. In: Eleventh USA\/Europe air traffic management research and development seminar (ATM)","DOI":"10.2514\/atcq.23.4.245"},{"key":"15_CR28","unstructured":"Leveson NG, Turner CS (1993) Investigation of the therac-25 accidents. IEEE Comput 26(7):18\u201341"},{"key":"15_CR29","doi-asserted-by":"publisher","unstructured":"Miller SP, Whalen MW, Cofer DD (2010) Software model checking takes off. Commun ACM 53(2):58\u201364. ISSN 0001-0782. doi: 10.1145\/1646353.1646372","DOI":"10.1145\/1646353.1646372"},{"key":"15_CR30","unstructured":"Navarre D, Palanque P, Bastide R (2001) Engineering interactive systems through formal methods for both tasks and system models. In Proceedings of the RTO Human Factors and Medicine Panel (HFM) specialists\u2019 meeting, pp 20.1\u201320.17, June 2001"},{"key":"15_CR31","doi-asserted-by":"crossref","unstructured":"Rungta N, Brat G, Clancey WJ, Linde C, Raimondi F, Seah C, Shafto M (2013) Aviation safety: modeling and analyzing complex interactions between humans and automated systems. In: Proceedings of the 3rd international conference on application and theory of automation in command and control systems. ACM, pp 27\u201337","DOI":"10.1145\/2494493.2494498"},{"key":"15_CR32","doi-asserted-by":"crossref","unstructured":"Rungta N, Mercer EG, Raimondi F, Krantz BC, Stocker R, Wallace A (2016) Modeling complex air traffic management systems. In: Proceedings of the 8th international workshop on modeling in software engineering. ACM, pp 41\u201347","DOI":"10.1145\/2896982.2896993"},{"key":"15_CR33","doi-asserted-by":"crossref","unstructured":"Rushby JM (2011) New challenges in certification for aircraft software. In: Chakraborty S, Jerraya A, Baruah SK, Fischmeister S (eds) EMSOFT. ACM, pp 211\u2013218. ISBN 978-1-4503-0714-7","DOI":"10.1145\/2038642.2038675"},{"key":"15_CR34","unstructured":"Sierhuis M (2001) Modeling and simulating work practice. BRAHMS: a multiagent modeling and simulation language for work system analysis and design. PhD thesis, Social Science and Informatics (SWI), University of Amsterdam, SIKS Dissertation Series No. 2001-10, Amsterdam, The Netherlands"},{"key":"15_CR35","unstructured":"Thimbleby H (2010) Press on: principles of interaction programming. The MIT Press, Jan 2010. ISBN 0262514230"},{"key":"15_CR36","unstructured":"Thimbleby H, Gow J (2007) Applying graph theory to interaction design. In Gulliksen J, Harning MB, Palanque P, van der Veer G, Wesson J (eds) Proceedings of the engineering interactive systems joint working conferences EHCI, DSV-IS, HCSE (EIS 2007). Lecture notes in computer science, vol 4940, pp 501\u2013519. Springer, Mar 2007"},{"key":"15_CR37","doi-asserted-by":"crossref","unstructured":"Tretmans J (2008) Model based testing with labelled transition systems. In: Hierons R, Bowen J, Harman M (eds) Formal methods and testing. Lecture notes in computer science, vol 4949. Springer, pp 1\u201338","DOI":"10.1007\/978-3-540-78917-8_1"},{"key":"15_CR38","unstructured":"uberlingeng (2004) Investigation Report AX001-1-2\/02. Technical report, German Federal Bureau of Aircraft Accidents Investigation"},{"key":"15_CR39","doi-asserted-by":"crossref","unstructured":"Yasmeen A, Gunter EL (2011) Automated framework for formal operator task analysis. In Dwyer MB, Tip F (eds) ISSTA. ACM, pp 78\u201388","DOI":"10.1145\/2001420.2001430"},{"key":"15_CR40","doi-asserted-by":"crossref","unstructured":"Young RM, Green TRG, Simon T (1989) Programmable user models for predictive evaluation of interface designs. In: ACM SIGCHI bulletin, vol 20. ACM, pp 15\u201319","DOI":"10.1145\/67449.67453"}],"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":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-51838-1_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,21]],"date-time":"2019-09-21T14:08:35Z","timestamp":1569074915000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-51838-1_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319518374","9783319518381"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-51838-1_15","relation":{},"ISSN":["1571-5035"],"issn-type":[{"value":"1571-5035","type":"print"}],"subject":[],"published":{"date-parts":[[2017]]}}}