{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,30]],"date-time":"2025-12-30T23:38:28Z","timestamp":1767137908570,"version":"build-2238731810"},"publisher-location":"Cham","reference-count":38,"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_8","type":"book-chapter","created":{"date-parts":[[2017,4,24]],"date-time":"2017-04-24T04:23:43Z","timestamp":1493007823000},"page":"211-245","source":"Crossref","is-referenced-by-count":1,"title":["Modelling the User"],"prefix":"10.1007","author":[{"given":"Paul","family":"Curzon","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rimvydas","family":"Ruk\u0161\u0117nas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,4,25]]},"reference":[{"issue":"1","key":"8_CR1","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1207\/s15516709cog2601_2","volume":"26","author":"E Altmann","year":"2002","unstructured":"Altmann E, Trafton J (2002) Memory for goals: an activation-based model. Cognit Sci 26(1):39\u201383","journal-title":"Cognit Sci"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Barnard PJ, May J (1995) Interactions with advanced graphical interfaces and the deployment of latent human knowledge. In: Interactive systems: design, specification, and verification (DSV-IS\u201995). Springer, pp 15\u201349","DOI":"10.1007\/978-3-642-87115-3_2"},{"issue":"5","key":"8_CR3","doi-asserted-by":"publisher","first-page":"563","DOI":"10.3233\/JCS-150536","volume":"23","author":"G Bella","year":"2015","unstructured":"Bella G, Curzon P, Lenzini G (2015) Service security and privacy as a socio-technical problem: literature review, analysis methodology and challenge domains. J Comput Secur 23(5):563\u2013585. doi:\n10.3233\/JCS-150536","journal-title":"J Comput Secur"},{"key":"8_CR4","doi-asserted-by":"crossref","first-page":"132","DOI":"10.1007\/s001650050045","volume":"11","author":"H Bowman","year":"2000","unstructured":"Bowman H, Faconti G (2000) Analysing cognitive behaviour using LOTOS and Mexitl. Formal Aspects Comput 11:132\u2013159","journal-title":"Formal Aspects Comput"},{"key":"8_CR5","unstructured":"Bredereke J, Lankenau A (2004) A rigorous view of mode confusion. In: Computer safety, reliability and security: SAFECOMP 2002. Lecture notes in computer science, vol 2434. Springer, pp 19\u201331"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Buth B (2004) Analysing mode confusion: an approach using FDR2. In: Computer safety, reliability and security: SAFECOMP 2004. Lecture notes in computer science, vol 3219. Springer, pp 101\u2013114","DOI":"10.1007\/978-3-540-30138-7_9"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Butterworth RJ, Blandford AE, Duke DJ (2000) Demonstrating the cognitive plausibility of interactive systems. Formal Aspects Comput 237\u2013259","DOI":"10.1007\/s001650070021"},{"issue":"1","key":"8_CR8","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1207\/s15516709cog2101_2","volume":"21","author":"M Byrne","year":"1997","unstructured":"Byrne M, Bovair S (1997) A working memory model of a common procedural error. Cognit Sci 21(1):31\u201361","journal-title":"Cognit Sci"},{"key":"8_CR9","unstructured":"Curzon P, Blandford A (2000) Using a verification system to reason about post-completion errors. In: Palanque P, Patern\u00f2 F (eds) Participants Proc. of DSV-IS 2000: 7th International workshop on design, specification and verification of interactive systems, at the 22nd International conference on software engineerings, pp 292\u2013308"},{"key":"8_CR10","doi-asserted-by":"publisher","unstructured":"Curzon P, Blandford A (2001) Detecting multiple classes of user errors. In: Little R, Nigay L (eds) Proceedings of the 8th IFIP working conference on engineering for human-computer interaction (EHCI\u201901). Lecture notes in computer science, vol 2254. Springer, pp 57\u201371. doi:\n10.1007\/3-540-45348-2_9","DOI":"10.1007\/3-540-45348-2_9"},{"key":"8_CR11","doi-asserted-by":"publisher","unstructured":"Curzon P, Blandford A (2002) From a formal user model to design rules. In: Forbrig P, Urban B, Vanderdonckt J, Limbourg Q (eds) 9th International workshop on interactive systems. Design, specification and verification. Lecture notes in computer science, vol 2545. Springer, pp 1\u201315. doi:\n10.1007\/3-540-36235-5_1","DOI":"10.1007\/3-540-36235-5_1"},{"key":"8_CR12","doi-asserted-by":"publisher","unstructured":"Curzon P, Blandford A (2004) Formally justifying user-centred design rules: a case study on post-completion errors. In: Boiten E, Derrick J, Smith G (eds) Proceedings of the 4th international conference on integrated formal methods. Lecture notes in computer science, vol 2999. Springer, pp 461\u2013480. doi:\n10.1007\/b96106","DOI":"10.1007\/b96106"},{"issue":"4","key":"8_CR13","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1007\/s00165-007-0035-6","volume":"19","author":"P Curzon","year":"2007","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:\n10.1007\/s00165-007-0035-6","journal-title":"Formal Aspects Comput"},{"key":"8_CR14","doi-asserted-by":"publisher","unstructured":"Curzon P, Blandford A, Thimbleby H, Cox A (2015) Safer interactive medical device design: Insights from the CHI+MED project. In: 5th EAI International conference on wireless mobile communication and healthcare\u2014Transforming healthcare through innovations in mobile and wireless technologies. ACM. doi:\n10.4108\/eai.14-10-2015.2261752","DOI":"10.4108\/eai.14-10-2015.2261752"},{"issue":"4","key":"8_CR15","doi-asserted-by":"crossref","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. Human Comput Interact 13(4):337\u2013393","journal-title":"Syndetic modelling. Human Comput Interact"},{"key":"8_CR16","doi-asserted-by":"crossref","first-page":"144","DOI":"10.1007\/978-1-84628-941-5_7","volume-title":"Maturing usability: quality in software","author":"D Furniss","year":"2008","unstructured":"Furniss D, Blandford A, Curzon P (2008) Usability work in professional website design: Insights from practitioners\u2019 perspectives. In: Law E, Hvannberg E, Cockton G, Vanderdonckt J (eds) Maturing usability: quality in software. Springer, Interaction and value, pp 144\u2013167"},{"issue":"3","key":"8_CR17","doi-asserted-by":"crossref","first-page":"461","DOI":"10.1037\/0033-295X.113.3.461","volume":"113","author":"W Gray","year":"2006","unstructured":"Gray W, Sims C, Fu W, Schoelles M (2006) The soft constraints hypothesis: a rational analysis approach to resource allocation for interactive behavior. Psychol Rev 113(3):461\u2013482","journal-title":"Psychol Rev"},{"key":"8_CR18","doi-asserted-by":"publisher","unstructured":"Harrison M, Campos JC, Ruk\u0161\u0117nas R, Curzon P (2016) Modelling information resources and their salience in medical device design. In: Engineering interactive computing systems. ACM, pp 194\u2013203. doi:\n10.1145\/2933242.2933250\n\n, honourable Mention Award:top 5% papers","DOI":"10.1145\/2933242.2933250"},{"issue":"4","key":"8_CR19","doi-asserted-by":"crossref","first-page":"320","DOI":"10.1145\/235833.236054","volume":"3","author":"B John","year":"1996","unstructured":"John B, Kieras D (1996) The GOMS family of user interface analysis techniques: comparison and contrast. ACM Trans Comput-Hum Interact 3(4):320\u2013351","journal-title":"ACM Trans Comput-Hum Interact"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"John BE, Prevas K, Salvucci DD, Koedinger K (2004) Predictive human performance modeling made easy. In: Proceedings of the SIGCHI conference on human factors in computing systems, CHI \u201904, ACM, pp 455\u2013462","DOI":"10.1145\/985692.985750"},{"key":"8_CR21","unstructured":"Lankenau A (2001) Avoiding mode confusion in service-robots. In: Integration of assistive technology in the information age, Proceedings of the 7th international conference on rehabilitation robotics. IOS Press, pp 162\u2013167"},{"issue":"2","key":"8_CR22","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 (2015a) Using PVS to support the analysis of distributed cognition systems. Innov Syst Softw Eng 11(2):113\u2013130. doi:\n10.1007\/s11334-013-0202-2","journal-title":"Innov Syst Softw Eng"},{"key":"8_CR23","doi-asserted-by":"publisher","unstructured":"Masci P, Curzon P, Thimbleby H (2015b) Early identification of software causes of use-related hazards in medical devices. In: 5th EAI International conference on wireless mobile communication and healthcare\u2014Transforming healthcare through innovations in mobile and wireless technologies. ACM. doi:\n10.4108\/eai.14-10-2015.2261754","DOI":"10.4108\/eai.14-10-2015.2261754"},{"key":"8_CR24","unstructured":"Newell A (1990) Unified theories of cognition. Harvard University Press"},{"key":"8_CR25","unstructured":"Nielsen J (2000) Why you only need to test with 5 users. \nhttp:\/\/www.nngroup.com\/articles\/why-you-only-need-to-test-with-5-users\/"},{"key":"8_CR26","unstructured":"Norman DA (2002) The design of everyday things. Basic Books"},{"key":"8_CR27","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/ijhc.2001.0471","volume":"55","author":"F Ritter","year":"2001","unstructured":"Ritter F, Young R (2001) Embodied models as simulated users: introduction to this special issue on using cognitive models to improve interface design. Int J Hum Comput Stud 55:1\u201314","journal-title":"Int J Hum Comput Stud"},{"key":"8_CR28","doi-asserted-by":"publisher","unstructured":"Ruk\u0161\u0117nas R, Curzon P, Blandford A (2007a) Detecting cognitive causes of confidentiality leaks. In: Curzon P, Cerone A (eds) Proceedings of the 1st International workshop on formal methods for interactive systems. Electronic notes in theoretical computer science, vol 183. Elsevier pp 21\u201338. doi:\n10.1016\/j.entcs.2007.01.059","DOI":"10.1016\/j.entcs.2007.01.059"},{"key":"8_CR29","doi-asserted-by":"publisher","unstructured":"Ruk\u0161\u0117nas R, Curzon P, Blandford A, Back J (2007b) Combining human error verification and timing analysis. In: Proceedings of engineering interactive systems 2007: Joining three working conferences IFIP WG2.7\/13.4 10th conference on engineering human computer interaction, IFIP WG 13.2 1st conference on human centered software engineering, DSVIS\u201414th conference on design specification and verification of interactive systems. Lecture notes in computer science, vol 4940. Springer, pp 18\u201335. doi:\n10.1007\/978-3-540-92698-6_2","DOI":"10.1007\/978-3-540-92698-6_2"},{"key":"8_CR30","doi-asserted-by":"publisher","unstructured":"Ruk\u0161\u0117nas R, Curzon P, Back J, Blandford A (2008a) Formal modelling of salience and cognitive load. Electron Notes Theoret Comput Sci 208:57\u201375. doi:\n10.1016\/j.entcs.2008.03.107","DOI":"10.1016\/j.entcs.2008.03.107"},{"issue":"2","key":"8_CR31","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/s11334-008-0050-7","volume":"30","author":"R Ruk\u0161\u0117nas","year":"2008","unstructured":"Ruk\u0161\u0117nas R, Curzon P, Blandford A (2008b) Modelling and analysing cognitive causes of security breaches. Innov Syst Softw Eng 30(2):143\u2013160. doi:\n10.1007\/s11334-008-0050-7","journal-title":"Innov Syst Softw Eng"},{"key":"8_CR32","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, Curzon P, Blandford A (2009) Verification-guided modelling of salience and cognitive load. Formal Aspects Comput 21:541\u2013569. doi:\n10.1007\/s00165-008-0102-7","journal-title":"Formal Aspects Comput"},{"key":"8_CR33","doi-asserted-by":"publisher","unstructured":"Ruk\u0161\u0117nas R, Curzon P, Harrison MD (2013) Integrating formal predictions of interactive system behaviour with user evaluation. In: Johnsen EB, Petre L (eds) Proceedings of integrated formal methods. LNCS, vol 7940. Springer, pp 238\u2013252. doi:\n10.1007\/978-3-642-38613-8_17","DOI":"10.1007\/978-3-642-38613-8_17"},{"issue":"5","key":"8_CR34","doi-asserted-by":"publisher","first-page":"1033","DOI":"10.1007\/s00165-013-0288-1","volume":"26","author":"R Ruk\u0161\u0117nas","year":"2014","unstructured":"Ruk\u0161\u0117nas R, Curzon P, Blandford A, Back J (2014) Combining human error verification and timing analysis: a case study on an infusion pump. Formal Aspects Comput 26(5):1033\u20131076. doi:\n10.1007\/s00165-013-0288-1","journal-title":"Formal Aspects Comput"},{"key":"8_CR35","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S1571-0661(04)80891-0","volume":"43","author":"J Rushby","year":"2001","unstructured":"Rushby J (2001) Analyzing cockpit interfaces using formal methods. Electron Notes Theoret Comput Sci 43:1\u201314. doi:\n10.1016\/S1571-0661(04)80891-0","journal-title":"Electron Notes Theoret Comput Sci"},{"issue":"2","key":"8_CR36","doi-asserted-by":"crossref","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 suprises. Reliab Eng System Safety 75(2):167\u2013177","journal-title":"Reliab Eng System Safety"},{"key":"8_CR37","doi-asserted-by":"crossref","first-page":"513","DOI":"10.1007\/s00165-008-0094-3","volume":"21","author":"L Su","year":"2009","unstructured":"Su L, Bowman H, Barnard P, Wyble B (2009) Process algebraic modelling of attentional capture and human electrophysiology in interactive systems. Formal Aspects Comput 21:513\u2013539","journal-title":"Formal Aspects Comput"},{"issue":"3","key":"8_CR38","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1006\/ijhc.2000.0442","volume":"54","author":"H Thimbleby","year":"2001","unstructured":"Thimbleby H (2001) Permissive user interfaces. Int J Hum-Comput Stud 54(3):333\u2013350. doi:\n10.1006\/ijhc.2000.0442","journal-title":"Int J Hum-Comput Stud"}],"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_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,7,28]],"date-time":"2017-07-28T07:03:39Z","timestamp":1501225419000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-51838-1_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319518374","9783319518381"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-51838-1_8","relation":{},"ISSN":["1571-5035"],"issn-type":[{"value":"1571-5035","type":"print"}],"subject":[],"published":{"date-parts":[[2017]]}}}