{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T13:51:39Z","timestamp":1772200299321,"version":"3.50.1"},"publisher-location":"Cham","reference-count":78,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783319276489","type":"print"},{"value":"9783319276489","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-319-27648-9_120-1","type":"book-chapter","created":{"date-parts":[[2025,4,7]],"date-time":"2025-04-07T08:30:49Z","timestamp":1744014649000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Formal Approaches for Interactive Systems"],"prefix":"10.1007","author":[{"given":"Jos\u00e9 Creissac","family":"Campos","sequence":"first","affiliation":[]},{"given":"Michael D.","family":"Harrison","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,4,8]]},"reference":[{"issue":"4","key":"120-1_CR1","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. Human\u2013Comput Interact 12(4):439\u2013462. https:\/\/doi.org\/10.1207\/s15327051hci1204_5","journal-title":"Human\u2013Comput Interact"},{"key":"120-1_CR2","unstructured":"Arney D (2019) Medical device interoperability with provable safety properties. PhD thesis, University of Pennsylvania"},{"key":"120-1_CR3","first-page":"25","volume-title":"Interactive systems: design, specification and verification (DSVIS 2006), no. 4323 in Springer lecture notes in computer science","author":"E Barboni","year":"2007","unstructured":"Barboni E, Conversy S, Navarre D, Palanque P (2007) Model-based engineering of widgets, user applications and servers compliant with ARINC 661 specification. In: Doherty G, Blandford A (eds) Interactive Systems: Design, Specification and Verification (DSV-IS 2006), no. 4323 in Lecture Notes in Computer Science. Springer, pp 25\u201338"},{"key":"120-1_CR4","volume-title":"Progress in the psychology of language","author":"P Barnard","year":"1985","unstructured":"Barnard P (1985) Interacting cognitive subsystems: a psycholinguistic approach to short-term memory. In: Ellis A (ed) Progress in the psychology of language, vol 2. Lawrence Erlbaum, pp 197\u2013258"},{"issue":"2","key":"120-1_CR5","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1145\/1061254.1061256","volume":"14","author":"J Berstel","year":"2005","unstructured":"Berstel J, Reghizzi S, Rouseel G, Pietro P (2005) A scalable formal method for the design and automatic checking of user interfaces. ACM Trans Softw Eng Methodol 14(2):124\u2013167","journal-title":"ACM Trans Softw Eng Methodol"},{"key":"120-1_CR6","volume-title":"Contextual design: defining customer-centred systems","author":"H Beyer","year":"1998","unstructured":"Beyer H, Holtzblatt K (1998) Contextual design: defining customer-centred systems. Morgan Kaufmann"},{"key":"120-1_CR7","first-page":"26","volume-title":"Proceedings DSVIS 2005, no. 3941 in Springer lecture notes in computer science","author":"A Blandford","year":"2006","unstructured":"Blandford A, Furniss D (2006) DiCoT: a methodology for applying distributed cognition to the design of team working systems. In: Gilroy SW, Harrison MD (eds) Proceedings DSVIS 2005, no. 3941 in Springer lecture notes in computer science. Springer, pp 26\u201338"},{"key":"120-1_CR8","first-page":"111","volume-title":"People and computers VIII","author":"A Blandford","year":"1993","unstructured":"Blandford A, Young R (1993) Developing runnable user models: separating the problem solving techniques from the domain knowledge. In: Alty J, Diaper D, Guest S (eds) People and computers VIII, Cambridge University Press, p. 111\u2013122"},{"key":"120-1_CR9","first-page":"45","volume-title":"Design, specification and verification of interactive systems\u201997","author":"A Blandford","year":"1997","unstructured":"Blandford A, Butterworth R, Good J (1997) Users as rational interacting agents: formalising assumptions about cognition and interaction. In: Harrison M, Torres J (eds) Design, specification and verification of interactive systems\u201997. Springer, pp 45\u201360"},{"issue":"1","key":"120-1_CR10","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/0169-7552(87)90085-7","volume":"14","author":"T Bolognesi","year":"1987","unstructured":"Bolognesi T, Brinksma E (1987) Introduction to the ISO specification language LOTOS. Comput Netw ISDN Syst 14(1):25\u201329","journal-title":"Comput Netw ISDN Syst"},{"key":"120-1_CR11","doi-asserted-by":"crossref","unstructured":"Bolton ML, Bass EJ (2017) Enhanced operator function model (EOFM): a task analytic modeling formalism for including human behavior in the verification of complex systems. In: Weyers et al. (2017), pp 343\u2013377, chap 13","DOI":"10.1007\/978-3-319-51838-1_13"},{"key":"120-1_CR12","doi-asserted-by":"crossref","unstructured":"Bolton M, Siminiceanu R, Bass E (2011) A systematic approach to model checking human\u2013automation interaction using task analytic models. IEEE Trans Syst Man Cybernetics, Part A: Syst Humans 41(5):961\u2013976","DOI":"10.1109\/TSMCA.2011.2109709"},{"issue":"3","key":"120-1_CR13","doi-asserted-by":"publisher","first-page":"488","DOI":"10.1109\/TSMCA.2012.2210406","volume":"43","author":"ML Bolton","year":"2013","unstructured":"Bolton ML, Bass E, Siminiceanu R (2013) Using formal verification to evaluate human-automation interaction: a review. IEEE Trans Syst Man Cybernetics, Part A: Syst Humans 43(3):488\u2013503","journal-title":"IEEE Trans Syst Man Cybernetics, Part A: Syst Humans"},{"issue":"5","key":"120-1_CR14","doi-asserted-by":"publisher","first-page":"561","DOI":"10.1109\/THMS.2014.2329476","volume":"44","author":"ML Bolton","year":"2014","unstructured":"Bolton ML, Jim\u00e9nez N, van Paassen MM, Trujillo M (2014) Automatically generating specification properties from task models for the formal verification of human-automation interaction. IEEE Trans Human-Machine Syst 44(5):561\u2013575","journal-title":"IEEE Trans Human-Machine Syst"},{"key":"120-1_CR15","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/s00165-008-0095-2","volume":"21","author":"J Bowen","year":"2009","unstructured":"Bowen J, Reeves S (2009) Refinement for user interface designs. Form Asp Comput 21:589\u2013612","journal-title":"Form Asp Comput"},{"key":"120-1_CR16","doi-asserted-by":"crossref","unstructured":"Bowen J, Reeves S (2017) Combining models for interactive system modelling. In: Weyers et al. (2017), pp 161\u2013182, chap 6","DOI":"10.1007\/978-3-319-51838-1_6"},{"key":"120-1_CR17","doi-asserted-by":"publisher","unstructured":"Bowen J, Dittmar A, Weyers B (2021) Task modelling for interactive system design: a survey of historical trends, gaps and future needs. In: Proceedings of ACM Human-Computer Interactions 5(EICS):1\u201322. https:\/\/doi.org\/10.1145\/3461736","DOI":"10.1145\/3461736"},{"key":"120-1_CR18","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/s11334-019-00333-7","volume":"15","author":"G Broccia","year":"2019","unstructured":"Broccia G, Milazzo P, \u00d6lveczky PC (2019) Formal modeling and analysis of safety-critical human multitasking. Innov Syst Softw Eng 15:169\u2013190","journal-title":"Innov Syst Softw Eng"},{"key":"120-1_CR19","first-page":"347","volume-title":"Design, specification and verification of interactive systems \u201996, Eurographics, proceedings of the Eurographics workshop in Namur, Belgium","author":"P Bumbulis","year":"1996","unstructured":"Bumbulis P, Alencar P, Cowan D, Lucena C (1996) Validating properties of component-based graphical user interfaces. In: Bodart F, Vanderdonckt J (eds) Design, specification and verification of interactive systems \u201996, Eurographics, proceedings of the Eurographics workshop in Namur, Belgium. Springer, Wien\/NewYork, pp 347\u2013365"},{"key":"120-1_CR20","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1023\/A:1011265604021","volume":"8","author":"JC Campos","year":"2001","unstructured":"Campos JC, Harrison MD (2001) Model checking interactor specifications. Autom Softw Eng 8:275\u2013310","journal-title":"Autom Softw Eng"},{"key":"120-1_CR21","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1016\/j.ijhcs.2013.10.005","volume":"72","author":"JC Campos","year":"2014","unstructured":"Campos JC, Doherty G, Harrison MD (2014) Analysing interactive devices based on information resource constraints. Int J Human-Comput Stud 72:284\u2013297","journal-title":"Int J Human-Comput Stud"},{"key":"120-1_CR22","doi-asserted-by":"publisher","unstructured":"Campos J, Fayollas C, Harrison M, Martinie C, Masci P, Palanque P (2020) Supporting the analysis of safety critical user interfaces: an exploration of three formal tools. ACM Trans Comput-Human Interact 27(5). https:\/\/doi.org\/10.1145\/3404199","DOI":"10.1145\/3404199"},{"key":"120-1_CR23","volume-title":"The psychology of human computer interaction","author":"SK Card","year":"1983","unstructured":"Card SK, Moran TP, Newell A (1983) The psychology of human computer interaction. Lawrence Erlbaum"},{"key":"120-1_CR24","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/s10270-007-0072-x","volume":"7","author":"A Cerone","year":"2008","unstructured":"Cerone A, Connelly S, Lindsay P (2008) Formal analysis of human operator behavioural patterns in interactive surveillance systems. Softw Syst Modeling 7:273\u2013286","journal-title":"Softw Syst Modeling"},{"issue":"2","key":"120-1_CR25","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/s11704-016-5460-3","volume":"12","author":"A Chebieb","year":"2018","unstructured":"Chebieb A, A\u00eft Ameur Y (2018) A formal model for plastic human computer interfaces. Front Comp Sci 12(2):351\u2013375","journal-title":"Front Comp Sci"},{"key":"120-1_CR26","volume-title":"Model checking","author":"EM Clarke","year":"1999","unstructured":"Clarke EM, Grumberg O, Peled DA (1999) Model checking. MIT Press"},{"issue":"2","key":"120-1_CR27","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1109\/THMS.2015.2424851","volume":"46","author":"S Comb\u00e9fis","year":"2016","unstructured":"Comb\u00e9fis S, Giannakopoulou D, Pecheur C (2016) Automatic detection of potential automation surprises for ADEPT models. IEEE Trans Human-Machine Syst 46(2):267\u2013278. https:\/\/doi.org\/10.1109\/THMS.2015.2424851","journal-title":"IEEE Trans Human-Machine Syst"},{"key":"120-1_CR28","first-page":"97","volume-title":"Formal methods in human computer interaction","author":"AJ Dix","year":"1990","unstructured":"Dix AJ (1990) Non determinism as a paradigm for understanding the user interface. In: Harrison MD, Thimbleby HW (eds) Formal methods in human computer interaction. Cambridge University Press, pp 97\u2013126"},{"issue":"4","key":"120-1_CR29","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/PL00003934","volume":"12","author":"G Doherty","year":"2000","unstructured":"Doherty G, Campos J, Harrison M (2000) Representational reasoning and verification. Form Asp Comput 12(4):260\u2013277","journal-title":"Form Asp Comput"},{"key":"120-1_CR30","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/978-3-540-70569-7_19","volume-title":"Interactive systems: design, specification and verification, DSVIS \u201908. Lecture notes in computer science","author":"G Doherty","year":"2008","unstructured":"Doherty G, Campos JC, Harrison MD (2008) Resources for situated actions. In: Graham N, Palanque P (eds) Interactive systems: design, specification and verification, DSVIS \u201908. Lecture notes in computer science, vol 5136. Springer, pp 194\u2013207"},{"issue":"3","key":"120-1_CR31","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1111\/1467-8659.1230025","volume":"12","author":"DJ Duke","year":"1993","unstructured":"Duke DJ, Harrison MD (1993) Abstract interaction objects. Comput Graphics Forum 12(3):25\u201336","journal-title":"Comput Graphics Forum"},{"issue":"4","key":"120-1_CR32","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1207\/s15327051hci1304_1","volume":"13","author":"DJ Duke","year":"1998","unstructured":"Duke DJ, Barnard PJ, Duce DA, May J (1998) Syndetic modelling. Hum Comput Interact 13(4):337\u2013393","journal-title":"Hum Comput Interact"},{"key":"120-1_CR33","doi-asserted-by":"crossref","unstructured":"Dwyer M, Avrunin G, Corbett J (1999) Patterns in property specifications for finite-state verification. In: 21st international conference on software engineering, Los Angeles, California, IEEE, pp 411\u2013420","DOI":"10.1145\/302405.302672"},{"key":"120-1_CR34","unstructured":"Fields RE (2001) Analysis of erroneous actions in the design of critical systems. PhD thesis, Department of Computer Science, University of York, Heslington, York, YO10 5DD"},{"key":"120-1_CR35","doi-asserted-by":"crossref","unstructured":"Gilmore S, Hillston J (1994) The PEPA workbench: a tool to support a process algebra-based approach to performance modelling. In: Proceedings of the seventh international conference on modelling techniques and tools for computer performance evaluation, no. 794 in Springer lecture notes in computer science. Springer, pp 353\u2013368","DOI":"10.1007\/3-540-58021-2_20"},{"key":"120-1_CR36","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1145\/1822018.1822041","volume-title":"Proceedings of the 2nd ACM SIGCHI symposium on engineering interactive computing systems","author":"A Gimblett","year":"2010","unstructured":"Gimblett A, Thimbleby H (2010) User interface model discovery: towards a generic approach. In: Proceedings of the 2nd ACM SIGCHI symposium on engineering interactive computing systems. ACM, New York, pp 145\u2013154. https:\/\/doi.org\/10.1145\/1822018.1822041"},{"issue":"6","key":"120-1_CR37","doi-asserted-by":"publisher","first-page":"1737","DOI":"10.1007\/s10270-023-01124-2","volume":"22","author":"M Gleirscher","year":"2023","unstructured":"Gleirscher M, van de Pol J, Woodcock J (2023) A manifesto for applicable formal methods. Softw Syst Model 22(6):1737\u20131749","journal-title":"Softw Syst Model"},{"key":"120-1_CR38","unstructured":"Hamon A, Palanque P, Deleris Y, Navarre D, Barboni E (2012) A tool-supported development process for bringing touch interactions into interactive cockpits for controlling embedded critical systems. In: International conference on Human-Computer Interaction in Aeronautics (HCI\u2019Aero 2012). Sep 2012, Brussels, Belgium. https:\/\/hal.science\/hal-03644335"},{"key":"120-1_CR39","doi-asserted-by":"publisher","unstructured":"Hamon A, Palanque P, Silva JL, Deleris Y, Barboni E (2013) Formal description of multi-touch interactions. In: Proceedings of the 5th ACM SIGCHI symposium on engineering interactive computing systems. Association for Computing Machinery, pp 207\u2013216. https:\/\/doi.org\/10.1145\/2494603.2480311","DOI":"10.1145\/2494603.2480311"},{"key":"120-1_CR40","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1007\/978-3-030-98388-8_28","volume-title":"Sense, feel, design","author":"MD Harrison","year":"2022","unstructured":"Harrison MD, Masci P (2022) Proving display conformance and action consistency: the example of an integrated clinical environment. In: Ardito C, Lanzilotti R, Malizia A, Larusdottir M, Spano LD, Campos JC, Hertzum M, Mentler T, Abdelnour Nocera J, Piccolo L, Sauer S, van der Veer G (eds) Sense, feel, design. Springer International Publishing, Cham, pp 316\u2013328"},{"key":"120-1_CR41","volume-title":"Formal methods in human computer interaction","year":"1990","unstructured":"Harrison MD, Thimbleby HW (eds) (1990) Formal methods in human computer interaction. Cambridge University Press"},{"issue":"2","key":"120-1_CR42","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/s11334-013-0201-3","volume":"11","author":"M Harrison","year":"2015","unstructured":"Harrison M, Campos J, Masci P (2015) Reusing models and properties in the analysis of similar interactive devices. Innov Syst Softw Eng 11(2):95\u2013111","journal-title":"Innov Syst Softw Eng"},{"key":"120-1_CR43","doi-asserted-by":"crossref","unstructured":"Harrison M, Campos J, Ruk\u0161\u0117nas R, Curzon P (2016) Modelling information resources and their salience in medical device design. In: EICS \u201916 Proceedings of the 8th ACM SIGCHI symposium on engineering interactive computing systems. ACM Press, pp 194\u2013203","DOI":"10.1145\/2933242.2933250"},{"issue":"6","key":"120-1_CR44","doi-asserted-by":"publisher","first-page":"834","DOI":"10.1109\/THMS.2017.2717910","volume":"47","author":"MD Harrison","year":"2017","unstructured":"Harrison MD, Masci P, Campos JC, Curzon P (2017) Verification of user interface software: the example of use-related safety requirements and programmable medical devices. IEEE Trans Human-Machine Syst 47(6):834\u2013846","journal-title":"IEEE Trans Human-Machine Syst"},{"issue":"8","key":"120-1_CR45","doi-asserted-by":"publisher","first-page":"802","DOI":"10.1109\/TSE.2018.2804939","volume":"45","author":"MD Harrison","year":"2018","unstructured":"Harrison MD, Masci P, Campos JC (2018) Verification templates for the analysis of user interface software design. IEEE Trans Softw Eng 45(8):802\u2013822","journal-title":"IEEE Trans Softw Eng"},{"key":"120-1_CR46","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/j.scico.2019.02.003","volume":"175","author":"MD Harrison","year":"2019","unstructured":"Harrison MD, Freitas L, Drinnan M, Campos JC, Masci P, di Maria C, Whitaker M (2019) Formal techniques in the safety analysis of software components of a new dialysis machine. Sci Comput Program 175:17\u201334","journal-title":"Sci Comput Program"},{"key":"120-1_CR47","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1207\/s15327051hci0701_1","volume":"7","author":"H Hartson","year":"1992","unstructured":"Hartson H, Gray P (1992) Temporal aspects of tasks in the user action notation. Human-Comput Interact 7:1\u201345","journal-title":"Human-Comput Interact"},{"key":"120-1_CR48","doi-asserted-by":"crossref","unstructured":"Houser AM, Bolton ML (2024) Formal mental models for human-centered cybersecurity. Int J Human\u2013Comput Interact 41(2):1414\u20131430. https:\/\/doi.org\/10.1080\/10447318.2024.2314353","DOI":"10.1080\/10447318.2024.2314353"},{"key":"120-1_CR49","volume-title":"Cognition in the wild","author":"E Hutchins","year":"1994","unstructured":"Hutchins E (1994) Cognition in the wild. MIT Press"},{"issue":"3\u20134","key":"120-1_CR50","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/s10009-007-0038-x","volume":"9","author":"K Jensen","year":"2007","unstructured":"Jensen K, Kristensen L, Wells L (2007) Coloured petri nets and CPN tools for modelling and validation of concurrent systems. Int J Softw Tools Technol Transfer (STTT) 9(3\u20134):213\u2013254","journal-title":"Int J Softw Tools Technol Transfer (STTT)"},{"key":"120-1_CR51","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1207\/s15327051hci1204_4","volume":"12","author":"D Kieras","year":"1997","unstructured":"Kieras D, Meyer D (1997) An overview of the epic architecture for cognition and performance with application to human-computer interaction. Human-Comput Interact 12:391\u2013438","journal-title":"Human-Comput Interact"},{"key":"120-1_CR52","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/3967.003.0009","volume-title":"An invitation to cognitive science, vol 4: methods, models, and conceptual issues","author":"JF Lehman","year":"1998","unstructured":"Lehman JF, Laird JE, Rosenbloom P (1998) A gentle introduction to soar: an architecture for human cognition. In: Osherson DN, Sternberg S, Scarborough D (eds) An invitation to cognitive science, vol 4: methods, models, and conceptual issues. MIT Press. https:\/\/doi.org\/10.7551\/mitpress\/3967.003.0009, chap 6"},{"key":"120-1_CR53","volume-title":"Engineering a safer world: systems thinking applied to safety (engineering systems)","author":"NG Leveson","year":"2011","unstructured":"Leveson NG (2011) Engineering a safer world: systems thinking applied to safety (engineering systems). MIT Press"},{"key":"120-1_CR54","doi-asserted-by":"publisher","unstructured":"Martinie C, Palanque P, Ragosta M, Fahssi R (2013) Extending procedural task models by systematic explicit integration of objects, knowledge and information. In: Proceedings of the 31st European conference on cognitive ergonomics, ECCE \u201913. Association for Computing Machinery, New York. https:\/\/doi.org\/10.1145\/2501907.2501954","DOI":"10.1145\/2501907.2501954"},{"key":"120-1_CR55","series-title":"Lecture notes in computer science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-642-33176-3_11","volume-title":"Software engineering for resilient systems","author":"P Masci","year":"2012","unstructured":"Masci P, Furniss D, Curzon P, Harrison MD, Blandford A (2012) Supporting field investigators with PVS: a case study in the healthcare domain. In: Avgeriou P (ed) Software engineering for resilient systems, Lecture notes in computer science, vol 7527. Springer, Berlin\/Heidelberg, pp 150\u2013164. https:\/\/doi.org\/10.1007\/978-3-642-33176-3_11"},{"key":"120-1_CR56","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-642-40793-2_21","volume-title":"Computer safety, reliability, and security","author":"P Masci","year":"2013","unstructured":"Masci P, Ayoub A, Curzon P, Lee I, Sokolsky O, Thimbleby H (2013) Model-based development of the generic pca infusion pump user interface prototype in pvs. In: Bitsch F, Guiochet J, Kaaniche M (eds) Computer safety, reliability, and security. Springer, Berlin\/Heidelberg, pp 228\u2013240"},{"key":"120-1_CR57","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/s11334-013-0202-2","volume":"11","author":"P Masci","year":"2015","unstructured":"Masci P, Curzon P, Furniss D, Blandford A (2015) Using pvs to support the analysis of distributed cognition systems. Innov Syst Softw Eng 11:113\u2013130","journal-title":"Innov Syst Softw Eng"},{"key":"120-1_CR58","first-page":"166","volume-title":"Engineering interactive systems, 5247","author":"M Massink","year":"2008","unstructured":"Massink M, Latella D, ter Beek MH, Harrison M, Loreti M (2008) A fluid flow approach to usability analysis of multi-user systems. In: Paterno F, Forbrig P (eds) Engineering interactive systems, 5247. Springer, pp 166\u2013180"},{"key":"120-1_CR59","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic model checking","author":"K McMillan","year":"1993","unstructured":"McMillan K (1993) Symbolic model checking. Kluwer"},{"issue":"4","key":"120-1_CR60","doi-asserted-by":"publisher","first-page":"18:1","DOI":"10.1145\/1614390.1614393","volume":"16","author":"D Navarre","year":"2009","unstructured":"Navarre D, Palanque, Ladry JFP, Barboni E (2009) ICOs: a model-based user interface description technique dedicated to interactive systems addressing usability, reliability and scalability. ACM Trans Comput-Human Interact 16(4):18:1\u201318:56. https:\/\/doi.org\/10.1145\/1614390.1614393","journal-title":"ACM Trans Comput-Human Interact"},{"key":"120-1_CR61","doi-asserted-by":"crossref","unstructured":"Nielsen J, Molich R (1990) Heuristic evaluation of user interfaces. In: Chew J, Whiteside J (eds) ACM CHI Proceedings CHI \u201990: empowering people, pp 249\u2013256","DOI":"10.1145\/97243.97281"},{"key":"120-1_CR62","doi-asserted-by":"crossref","unstructured":"Oliveira R, Palanque P, Weyers B, Bowen J, Dix A (2017) State of the art on formal methods for interactive systems. In: The handbook of formal methods in human-computer interaction, pp 3\u201355","DOI":"10.1007\/978-3-319-51838-1_1"},{"key":"120-1_CR63","first-page":"22","volume-title":"Theorem proving in higher order logics, TPHOLs 2008. Lecture notes in computer science","author":"S Owre","year":"2008","unstructured":"Owre S, Shankar N (2008) A brief overview of PVS. In: Mohamed OA, Munoz C, Tahar S (eds) Theorem proving in higher order logics, TPHOLs 2008. Lecture notes in computer science, vol 5170. Springer, Montreal, pp 22\u201327"},{"key":"120-1_CR64","volume-title":"Formal methods in human-computer interaction. Formal approaches to computing and information technology (FACIT)","year":"1998","unstructured":"Palanque P, Patern\u00f2 F (eds) (1998) Formal methods in human-computer interaction. Formal approaches to computing and information technology (FACIT). Springer"},{"key":"120-1_CR65","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-0445-2","volume-title":"Model-based design and evaluation of interactive applications","author":"F Patern\u00f2","year":"2000","unstructured":"Patern\u00f2 F (2000) Model-based design and evaluation of interactive applications. Springer, London\/Berlin\/Heidelberg"},{"key":"120-1_CR66","first-page":"155","volume-title":"People and computers VII: HCI \u201892 conference, BCS HCI Specialist Group","author":"F Patern\u00f2","year":"1992","unstructured":"Patern\u00f2 F, Faconti G (1992) On the use of LOTOS to describe graphical interaction. In: Monk A, Diaper D, Harrison MD (eds) People and computers VII: HCI \u201892 conference, BCS HCI Specialist Group. Cambridge University Press, pp 155\u2013174"},{"issue":"4","key":"120-1_CR67","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1093\/comjnl\/46.4.340","volume":"6","author":"F Patern\u00f2","year":"2003","unstructured":"Patern\u00f2 F, Santoro C (2003) Support for reasoning about interactive systems through human-computer interaction designers\u2019 representations. Comput J 6(4):340\u2013357","journal-title":"Comput J"},{"issue":"5","key":"120-1_CR68","doi-asserted-by":"publisher","first-page":"741","DOI":"10.1016\/0020-7373(92)90039-N","volume":"36","author":"PG Polson","year":"1992","unstructured":"Polson PG, Lewis C, Rieman J, Wharton C (1992) Cognitive walkthroughs: a method for theory-based evaluation of user interfaces. Int J Man-Machine Stud 36(5):741\u2013773","journal-title":"Int J Man-Machine Stud"},{"key":"120-1_CR69","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1007\/s00165-008-0102-7","volume":"21","author":"R Ruk\u0161\u0117nas","year":"2009","unstructured":"Ruk\u0161\u0117nas R, Back J, Curzon P, Blandford A (2009) Verification-guided modelling of salience and cognitive load. Form Asp Comput 21:541\u2013569","journal-title":"Form Asp Comput"},{"key":"120-1_CR70","doi-asserted-by":"publisher","unstructured":"Ruk\u0161\u0117nas R, Curzon P, Blandford A, Back J (2013) Combining human error verification and timing analysis: a case study on an infusion pump. Form Asp Comput:1\u201344. https:\/\/doi.org\/10.1007\/s00165-013-0288-1","DOI":"10.1007\/s00165-013-0288-1"},{"issue":"2","key":"120-1_CR71","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1016\/S0951-8320(01)00092-8","volume":"75","author":"J Rushby","year":"2002","unstructured":"Rushby J (2002) Using model checking to help discover mode confusions and other automation surprises. Reliab Eng Syst Saf 75(2):167\u2013177","journal-title":"Reliab Eng Syst Saf"},{"key":"120-1_CR72","doi-asserted-by":"publisher","first-page":"569","DOI":"10.1007\/3-540-54415-1_65","volume-title":"Theoretical aspects of computer software, Springer lecture notes in computer science","author":"M Ryan","year":"1991","unstructured":"Ryan M, Fiadeiro J, Maibaum T (1991) Sharing actions and attributes in modal action logic. In: Theoretical aspects of computer software, Springer lecture notes in computer science, vol 526. Springer, pp 569\u2013593"},{"issue":"7","key":"120-1_CR73","doi-asserted-by":"publisher","DOI":"10.1002\/smr.2439","volume":"35","author":"NK Singh","year":"2023","unstructured":"Singh NK, A\u00eft-Ameur Y, Mendil I, M\u00e9ry D, Navarre D, Palanque P, Pantel M (2023) F3fluid: a formal framework for developing safety- critical interactive systems in fluid. J Softw: Evol Process 35(7):e2439. https:\/\/doi.org\/10.1002\/smr.2439, https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/smr.2439","journal-title":"J Softw: Evol Process"},{"key":"120-1_CR74","volume-title":"Press on: principles of interaction programming","author":"H Thimbleby","year":"2007","unstructured":"Thimbleby H (2007) Press on: principles of interaction programming. MIT Press"},{"key":"120-1_CR75","doi-asserted-by":"publisher","DOI":"10.1201\/b12457","volume-title":"Cognitive work analysis","author":"K Vicente","year":"1999","unstructured":"Vicente K (1999) Cognitive work analysis. Lawrence Erlbaum Associates"},{"key":"120-1_CR76","volume-title":"The handbook of formal methods in human-computer interaction. Human-computer interaction series","year":"2017","unstructured":"Weyers B, Bowen J, Dix A, Palanque P (eds) (2017) The handbook of formal methods in human-computer interaction. Human-computer interaction series. Springer"},{"issue":"1","key":"120-1_CR77","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1207\/S15327051HCI1501_01","volume":"15","author":"P Wright","year":"2000","unstructured":"Wright P, Fields R, Harrison M (2000) Analyzing human-computer interaction as distributed cognition: the resources model. Human-Comput Interact 15(1):1\u201342","journal-title":"Human-Comput Interact"},{"key":"120-1_CR78","doi-asserted-by":"crossref","unstructured":"Young RM, Green TRG, Simon T (1989) Programmable user models for predictive evaluation of interface designs. In: Proceedings of CHI\u201989 conference on computer-human interaction, pp 15\u201319","DOI":"10.1145\/67449.67453"}],"container-title":["Handbook of Human Computer Interaction"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-27648-9_120-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,7]],"date-time":"2025-04-07T15:11:55Z","timestamp":1744038715000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-27648-9_120-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783319276489","9783319276489"],"references-count":78,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-27648-9_120-1","relation":{},"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"8 October 2024, 00:00:00","order":1,"name":"received","label":"Received","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"14 October 2024, 00:00:00","order":2,"name":"accepted","label":"Accepted","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"8 April 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}