{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T20:32:54Z","timestamp":1742934774320,"version":"3.40.3"},"publisher-location":"Cham","reference-count":62,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319518374"},{"type":"electronic","value":"9783319518381"}],"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_20","type":"book-chapter","created":{"date-parts":[[2017,4,24]],"date-time":"2017-04-24T04:23:43Z","timestamp":1493007823000},"page":"549-575","source":"Crossref","is-referenced-by-count":2,"title":["Dealing with Faults During Operations: Beyond Classical Use of Formal Methods"],"prefix":"10.1007","author":[{"given":"Camille","family":"Fayollas","sequence":"first","affiliation":[]},{"given":"Philippe","family":"Palanque","sequence":"additional","affiliation":[]},{"given":"Jean-Charles","family":"Fabre","sequence":"additional","affiliation":[]},{"given":"C\u00e9lia","family":"Martinie","sequence":"additional","affiliation":[]},{"given":"Yannick","family":"D\u00e9l\u00e9ris","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,4,25]]},"reference":[{"key":"20_CR1","unstructured":"Airlines Electronic Engineering Committee (2002) ARINC Specification 661: cockpit display system interfaces to user systems"},{"key":"20_CR2","unstructured":"Airlines Electronic Engineering Committee (2003) ARINC Specification 653: avionics application software standard interface"},{"issue":"2","key":"20_CR3","doi-asserted-by":"crossref","first-page":"166","DOI":"10.1109\/32.44380","volume":"16","author":"J Arlat","year":"1990","unstructured":"Arlat J, Aguera M, Amat L et al (1990) Fault injection for dependability validation: a methodology and some applications. IEEE Trans Softw Eng 16(2):166\u2013182","journal-title":"IEEE Trans Softw Eng"},{"issue":"1","key":"20_CR4","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1109\/TDSC.2004.2","volume":"1","author":"A Avi\u017eienis","year":"2004","unstructured":"Avi\u017eienis A, Laprie JC, Randell B, Landwehr C (2004) Basic concepts and taxonomy of dependable and secure computing. IEEE Trans Dependable Secure Comput 1(1):11\u201333","journal-title":"IEEE Trans Dependable Secure Comput"},{"key":"20_CR5","unstructured":"Barboni E, Conversy S, Navarre D, Palanque P (2006) Model-based engineering of widgets, user applications and servers compliant with ARINC 661 specification. In: Interactive systems. Design, specification, and verification. Springer, Berlin, Heidelberg, pp 25\u201338"},{"issue":"12","key":"20_CR6","doi-asserted-by":"crossref","first-page":"1502","DOI":"10.1016\/j.ress.2006.01.014","volume":"91","author":"S Basnyat","year":"2006","unstructured":"Basnyat S, Chozos N, Palanque P (2006) Multidisciplinary perspective on accident investigation. Reliab Eng Syst Saf 91(12):1502\u20131520","journal-title":"Reliab Eng Syst Saf"},{"issue":"5","key":"20_CR7","doi-asserted-by":"crossref","first-page":"545","DOI":"10.1016\/j.ssci.2007.01.001","volume":"45","author":"S Basnyat","year":"2007","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","journal-title":"Saf Sci"},{"key":"20_CR8","unstructured":"Bass L, Little R, Pellegrino R, Reed S, Seacord R, Sheppard S, Szezur MR (1991) The arch model: Seeheim revisited. UI Developpers\u2019 WorNshop, 1"},{"issue":"1","key":"20_CR9","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1109\/MS.1984.233702","volume":"1","author":"BW Boehm","year":"1984","unstructured":"Boehm BW (1984) Verifying and validating software requirements and design specifications. IEEE Softw 1(1):75","journal-title":"IEEE Softw"},{"issue":"7","key":"20_CR10","first-page":"476","volume":"12","author":"ML Bolton","year":"2015","unstructured":"Bolton ML (2015) Model checking human-human communication protocols using task models and miscommunication generation. J Aerosp Inf Syst 12(7):476\u2013489","journal-title":"J Aerosp Inf Syst"},{"issue":"6","key":"20_CR11","doi-asserted-by":"crossref","first-page":"1314","DOI":"10.1109\/TSMC.2013.2256129","volume":"43","author":"ML Bolton","year":"2013","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","journal-title":"IEEE Trans Syst Man Cybern: Syst"},{"issue":"11","key":"20_CR12","doi-asserted-by":"crossref","first-page":"888","DOI":"10.1016\/j.ijhcs.2012.05.010","volume":"70","author":"ML Bolton","year":"2012","unstructured":"Bolton ML, Bass EJ, Siminiceanu RI (2012) Generating phenotypical erroneous human behavior to evaluate human\u2013automation interaction using model checking. Int J Human Comput Stud 70(11):888\u2013906","journal-title":"Int J Human Comput Stud"},{"issue":"6","key":"20_CR13","doi-asserted-by":"crossref","first-page":"591","DOI":"10.1016\/j.ress.2010.02.002","volume":"95","author":"RL Boring","year":"2010","unstructured":"Boring RL, Hendrickson SM, Forester JA, Tran TQ, Lois E (2010) Issues in benchmarking human reliability analysis methods: a literature review. Reliab Eng Syst Saf 95(6):591\u2013605","journal-title":"Reliab Eng Syst Saf"},{"key":"20_CR14","doi-asserted-by":"crossref","unstructured":"Bowen J, Reeves S (2012) Modelling user manuals of modal medical devices and learning from the experience. In: Proceedings of ACM symposium on engineering interactive computing systems. ACM, pp 121\u2013130","DOI":"10.1145\/2305484.2305505"},{"issue":"4","key":"20_CR15","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1049\/sej.1993.0025","volume":"8","author":"J Bowen","year":"1993","unstructured":"Bowen J, Stavridou V (1993) Formal methods, safety-critical systems and standards. Softw Eng J 8(4):189\u2013209","journal-title":"Softw Eng J"},{"key":"20_CR16","unstructured":"Dearden AM, Harrison MD (1995) Formalising human error resistance and human error tolerance. In: Proceedings of the fifth international conference on human-machine interaction and artificial intelligence in aerospace, EURISCO"},{"key":"20_CR17","unstructured":"Department of the Army (2006) TM 5\u2013698-4, Failure modes, effects and criticality analysis (FMECA) for command, control, communications, computer, intelligence, surveillance, and reconnaissance (C4ISR) facilities"},{"key":"20_CR18","doi-asserted-by":"crossref","unstructured":"Dessiatnikoff A, Nicomette V, Alata E, Deswarte Y, Leconte B, Combes A, Simache C (2013) Securing integrated modular avionics computers. In Proceedings of the 32nd digital avionics system conference (DASC), Syracuse (NY, USA), 6\u201310 Oct","DOI":"10.1109\/DASC.2013.6712577"},{"issue":"3","key":"20_CR19","doi-asserted-by":"crossref","first-page":"202","DOI":"10.1504\/IJCCBS.2013.058407","volume":"4","author":"C Fayollas","year":"2013","unstructured":"Fayollas C, Fabre JC, Palanque P, Barboni E, Navarre D, Deleris Y (2013) Interactive cockpits as critical applications: a model-based and a fault-tolerant approach. Int J Crit Comput-Based Syst 4(3):202\u2013226","journal-title":"Int J Crit Comput-Based Syst"},{"key":"20_CR20","doi-asserted-by":"crossref","unstructured":"Fayollas C, Fabre JC, Palanque P, Cronel M, Navarre D, Deleris Y (2014) A software-implemented fault-tolerance approach for control and display systems in avionics. In Proceedings of the IEEE 20th Pacific rim international symposium on dependable computing, pp 21\u201330","DOI":"10.1109\/PRDC.2014.11"},{"key":"20_CR21","doi-asserted-by":"crossref","unstructured":"Genrich HJ (1991) Predicate\/transitions nets. In: Jensen K, Rozenberg G (eds) High-levels petri nets: theory and application. Springer, Heidelberg, pp 3\u201343","DOI":"10.1007\/978-3-642-84524-6_1"},{"issue":"5","key":"20_CR22","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1109\/52.57887","volume":"7","author":"A Hall","year":"1990","unstructured":"Hall A (1990) Seven myths of formal methods. IEEE Softw 7(5):11\u201319","journal-title":"IEEE Softw"},{"issue":"3","key":"20_CR23","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1109\/MSPEC.1986.6371028","volume":"23","author":"MH Hamilton","year":"1986","unstructured":"Hamilton MH (1986) Zero-defect software: the elusive goal: it is theoretically possible but difficult to achieve; logic and interface errors are most common, but errors in user intent may also occur. IEEE Spectr 23(3):47\u201353","journal-title":"IEEE Spectr"},{"key":"20_CR24","doi-asserted-by":"crossref","unstructured":"Hamon A, Palanque P, Silva JL, Deleris Y, Barboni E (2013) Formal description of multi-touch interactions. In: Symposium on engineering interactive computing systems. ACM, pp 207\u2013216","DOI":"10.1145\/2494603.2480311"},{"key":"20_CR25","unstructured":"Hecht H, Fiorentino E (1987) Reliability assessment of spacecraft electronics. In: Annual reliability and maintainability symposium. IEEE, pp 341\u2013346"},{"key":"20_CR26","unstructured":"Hollnagel E (2004) Barriers and accident prevention. Ashgage"},{"key":"20_CR27","unstructured":"IBM (1989) Common user access: advanced interface design guide. IBM, SC26-4582-0"},{"issue":"3","key":"20_CR29","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1016\/0020-7373(92)90059-T","volume":"37","author":"C Johnson","year":"1992","unstructured":"Johnson C, Harrison M (1992) Using temporal logic to support the specification and prototyping of interactive control systems. Int J Man Mach Stud 37(3):357\u2013385","journal-title":"Int J Man Mach Stud"},{"key":"20_CR30","doi-asserted-by":"crossref","unstructured":"Karlesky M, Isbister K (2013) Fidget widgets: secondary playful interactions in support of primary serious tasks. In CHI \u201913 extended abstracts on human factors in computing systems. ACM, pp 1149\u20131154","DOI":"10.1145\/2468356.2468561"},{"issue":"7","key":"20_CR31","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1109\/2.56851","volume":"23","author":"JC Laprie","year":"1990","unstructured":"Laprie JC, Arlat J, B\u00e9ounes C, Kanoun K (1990) Definition and analysis of hardware and software fault-tolerant architectures. IEEE Comput 23(7):39\u201351","journal-title":"IEEE Comput"},{"key":"20_CR32","doi-asserted-by":"crossref","unstructured":"Martinie C, Navarre D, Palanque P, Fayollas C (2015) A generic tool-supported framework for coupling task models and interactive applications. In Proceedings of the 7th ACM SIGCHI symposium on engineering interactive computing systems. ACM, pp 244\u2013253","DOI":"10.1145\/2774225.2774845"},{"issue":"2","key":"20_CR33","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1109\/THMS.2014.2365956","volume":"46","author":"C Martinie","year":"2016","unstructured":"Martinie C, Palanque P, Fahssi R, Blanquart JP, Fayollas C, Seguin C (2016) Task model-based systematic analysis of both system failures and human errors. IEEE Trans Human-Mach Syst 46(2):243\u2013254","journal-title":"IEEE Trans Human-Mach Syst"},{"key":"20_CR34","doi-asserted-by":"crossref","unstructured":"Martinie C, Palanque P, Navarre D, Barboni E (2012) A development process for usable large scale interactive critical systems: application to satellite ground segments. In Proceedings of the 4th international conference on human-centered software engineering. Springer, Berlin, Heidelberg, pp 72\u201393","DOI":"10.1007\/978-3-642-34347-6_5"},{"key":"20_CR35","doi-asserted-by":"crossref","unstructured":"Martinie C, Palanque P, Navarre D, Winckler M, Poupart E (2011) Model-based training: an approach supporting operability of critical interactive systems. In Proceedings of ACM symposium on engineering interactive computing systems. ACM, pp 53\u201362","DOI":"10.1145\/1996461.1996495"},{"issue":"2","key":"20_CR36","doi-asserted-by":"crossref","first-page":"144","DOI":"10.1109\/32.908959","volume":"27","author":"AM Memon","year":"2001","unstructured":"Memon AM, Pollack EM, Soffa ML (2001) Hierarchical GUI test case generation using automated planning. IEEE Trans Softw Eng 27(2):144\u2013155","journal-title":"IEEE Trans Softw Eng"},{"key":"20_CR37","unstructured":"Navarre D, Palanque P, Basnyat S (2008) usability service continuation through reconfiguration of input and output devices in safety critical interactive systems. The 27th international conference on computer safety, reliability and security. LNCS 5219, pp 373\u2013386"},{"issue":"4","key":"20_CR38","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1614390.1614393","volume":"16","author":"D Navarre","year":"2009","unstructured":"Navarre D, Palanque P, Ladry J, Barboni E (2009) ICOs: a model-based user interface description technique dedicated to interactive systems addressing usability, reliability and scalability. ACM TOCHI 16(4):1\u201356","journal-title":"ACM TOCHI"},{"key":"20_CR39","doi-asserted-by":"crossref","unstructured":"Nicolescu B, Peronnard P, Velazco R, Savaria Y (2003) Efficiency of transient bit-flips detection by software means: a complete study. In: Proceedings of the 18th IEEE international symposium on defect and fault tolerance in VLSI systems. IEEE, pp 377\u2013384","DOI":"10.1109\/DFTVS.2003.1250134"},{"issue":"2","key":"20_CR40","doi-asserted-by":"crossref","first-page":"461","DOI":"10.1109\/23.490893","volume":"43","author":"E Normand","year":"1996","unstructured":"Normand E (1996) Single-event effects in avionics. IEEE Trans Nucl Sci 43(2):461\u2013474","journal-title":"IEEE Trans Nucl Sci"},{"key":"20_CR41","doi-asserted-by":"crossref","unstructured":"Palanque P, Basnyat S (2004) Task patterns for taking into account in an efficient and systematic way both standard and erroneous user behaviours. In: 6th international conference on human error, safety and system development. Springer, pp 123\u2013139","DOI":"10.1007\/1-4020-8153-7_8"},{"key":"20_CR42","doi-asserted-by":"crossref","unstructured":"Palanque P, Bastide R (1995) Verification of an interactive software by analysis of its formal specification. In: Proceedings of the IFIP TC 13 human-computer interaction conference, Lillehammer, Norway, 27\u201329 June 1995, pp 191\u2013197","DOI":"10.1007\/978-1-5041-2896-4_32"},{"key":"20_CR43","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1016\/S0953-5438(97)00013-1","volume":"9","author":"P Palanque","year":"1997","unstructured":"Palanque P, Bastide R (1997) Synergistic modelling of tasks, users and systems using formal specification techniques. Interact Comput 9:129\u2013153","journal-title":"Interact Comput"},{"key":"20_CR44","unstructured":"Palanque P, Bastide R, Dourte L (1993) Contextual help for free with formal dialogue design. In: Proceedings of the fifth international conference on human-computer interaction, Orlando, Florida, USA, 8\u201313 Aug, p 2"},{"key":"20_CR45","doi-asserted-by":"crossref","unstructured":"Palanque P, Ladry JF, Navarre D, Barboni E (2009) High-fidelity prototyping of interactive systems can be formal too. 13th international conference on human-computer interaction San Diego, CA, USA, LNCS, pp 667\u2013676","DOI":"10.1007\/978-3-642-02574-7_75"},{"key":"20_CR46","doi-asserted-by":"crossref","unstructured":"Pnueli A (1986) Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends. LNCS n\u00b0 224. Springer, pp 510\u2013584","DOI":"10.1007\/BFb0027047"},{"issue":"3","key":"20_CR47","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/s101110200016","volume":"4","author":"P Polet","year":"2002","unstructured":"Polet P, Vanderhaegen F, Wieringa P (2002) Theory of safety related violation of system barriers. Cogn Technol Work 4(3):171\u2013179","journal-title":"Cogn Technol Work"},{"key":"20_CR48","doi-asserted-by":"crossref","unstructured":"Rajkomar A, Blandford A (2012) A distributed cognition model for analysing interruption resumption during infusion administration. In Proceedings of the 30th European conference on cognitive ergonomics. ACM, pp 108\u2013111","DOI":"10.1145\/2448136.2448159"},{"key":"20_CR49","doi-asserted-by":"crossref","unstructured":"Reason J (1990) Human error. Cambridge University Press","DOI":"10.1017\/CBO9781139062367"},{"issue":"2","key":"20_CR50","doi-asserted-by":"crossref","first-page":"138","DOI":"10.1145\/317087.317088","volume":"2","author":"MK Reiter","year":"1999","unstructured":"Reiter MK, Stubblebine SG (1999) Authentication metric analysis and design. ACM Trans Inf Syst Secur 2(2):138\u2013158","journal-title":"ACM Trans Inf Syst Secur"},{"key":"20_CR51","unstructured":"RTCA and EUROCAE (2000) DO-254\u2014design assurance guidance for airborne electronic hardware"},{"key":"20_CR52","unstructured":"RTCA and EUROCAE (2011) DO-333 formal methods supplement to DO-178C and DO-278A software tool qualification considerations"},{"key":"20_CR53","unstructured":"RTCA and EUROCAE (2012) DO-178C\/ ED-12C, Software considerations in airborne systems and equipment certification"},{"issue":"6","key":"20_CR54","doi-asserted-by":"crossref","first-page":"541","DOI":"10.1007\/s00165-008-0102-7","volume":"21","author":"R Ruksenas","year":"2009","unstructured":"Ruksenas R, Back J, Curzon P, Blandford A (2009) Verification-guided modelling of salience and cognitive load. Formal Asp Comput 21(6):541\u2013569","journal-title":"Formal Asp Comput"},{"key":"20_CR55","doi-asserted-by":"crossref","unstructured":"Schroeder B, Pinheiro E, Weber WD (2009) DRAM errors in the wild: a large-scale field study. In ACM SIGMETRICS, pp 193\u2013204","DOI":"10.1145\/1555349.1555372"},{"key":"20_CR56","unstructured":"Stavely AM (1998) Toward zero-defect programming, 1st edn. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA"},{"key":"20_CR57","doi-asserted-by":"crossref","unstructured":"Tankeu-Choitat A, Fabre JC, Palanque P, Navarre D, Deleris Y (2011a) Self-checking components for dependable interactive cockpits. In: Working conference on dependable computing, ACM","DOI":"10.1109\/PRDC.2011.28"},{"key":"20_CR58","doi-asserted-by":"crossref","unstructured":"Tankeu-Choitat A, Navarre D, Palanque P, Deleris Y, Fabre JC, Fayollas C (2011b) Self-checking components for dependable interactive cockpits using formal description techniques. In: Proceedings of 17th IEEE Pacific rim international symposium on dependable computing","DOI":"10.1109\/PRDC.2011.28"},{"key":"20_CR59","unstructured":"Thimbleby H, Gimblett A (2011) Dependable keyed data entry for interactive systems. In: Proceedings of the 4th international workshop on formal methods for interactive systems"},{"key":"20_CR60","doi-asserted-by":"crossref","unstructured":"Traverse P, Lacaze I, Souyris J (2004) Airbus fly-by-wire: a total approach to dependability. In: Proceedings of the 18th IFIP world computer congress, building the information society, pp 191\u2013212","DOI":"10.1007\/978-1-4020-8157-6_18"},{"key":"20_CR61","doi-asserted-by":"crossref","unstructured":"Wright N, Patrick AS, Biddle R (2012) Do you see your password?: applying recognition to textual passwords. In: Proceedings of symposium on usable privacy and security. ACM","DOI":"10.1145\/2335356.2335367"},{"key":"20_CR62","doi-asserted-by":"crossref","unstructured":"Yau SS, Cheung RC (1975) Design of self-checking software. In Proceedings of the international conference on reliable software. IEEE, pp 450\u2013457","DOI":"10.1145\/800027.808468"},{"key":"20_CR63","doi-asserted-by":"crossref","unstructured":"Yeh YC (1996) Triple-triple redundant 777 primary flight computer. In: IEEE aerospace applications conference, pp 293\u2013307","DOI":"10.1109\/AERO.1996.495891"}],"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_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,21]],"date-time":"2019-09-21T14:09:02Z","timestamp":1569074942000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-51838-1_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319518374","9783319518381"],"references-count":62,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-51838-1_20","relation":{},"ISSN":["1571-5035"],"issn-type":[{"type":"print","value":"1571-5035"}],"subject":[],"published":{"date-parts":[[2017]]}}}