{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,26]],"date-time":"2025-10-26T22:51:23Z","timestamp":1761519083859},"reference-count":39,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2014,9,1]],"date-time":"2014-09-01T00:00:00Z","timestamp":1409529600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2014,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            The design of a human\u2013computer interactive system can be unacceptable for a range of reasons. User performance concerns, for example the likelihood of user errors and time needed for a user to complete tasks, are important areas of consideration. For safety-critical systems it is vital that tools are available to support the analysis of such properties before expensive design commitment has been made. In this work, we give a unified formal verification framework for integrating two kinds of analysis: (1) predicting bounds for task-completion times via exhaustive state-space exploration, and (2) detecting user-error related design issues. The framework is based on a generic model of cognitively plausible behaviour that captures assumptions about cognitive behaviour decided through a process of interdisciplinary negotiation. Assumptions made in an analysis, including those relating to the performance consequences of users\n            <jats:italic>recovering<\/jats:italic>\n            from likely errors, are also investigated in this framework. We further present a novel way of exploring the consequences of cognitive mismatches, on both correctness and performance grounds. We illustrate our analysis approach with a realistic medical device scenario: programming an infusion pump. We explore an initial pump design and then two variations based on features found in real designs, illustrating how the approach identifies both timing and human error issues.\n          <\/jats:p>","DOI":"10.1007\/s00165-013-0288-1","type":"journal-article","created":{"date-parts":[[2013,11,8]],"date-time":"2013-11-08T06:51:42Z","timestamp":1383893502000},"page":"1033-1076","source":"Crossref","is-referenced-by-count":12,"title":["Combining human error verification and timing analysis: a case study on an infusion pump"],"prefix":"10.1145","volume":"26","author":[{"given":"Rimvydas","family":"Ruk\u0161\u0117nas","sequence":"first","affiliation":[{"name":"School of Electronic Engineering and Computer Science, Queen Mary University of London, Mile End, E1 4NS, London, UK"}]},{"given":"Paul","family":"Curzon","sequence":"additional","affiliation":[{"name":"School of Electronic Engineering and Computer Science, Queen Mary University of London, Mile End, E1 4NS, London, UK"}]},{"given":"Ann","family":"Blandford","sequence":"additional","affiliation":[{"name":"UCL Interaction Centre, MPEB, University College London, Gower Street, WC1E 6BT, London, UK"}]},{"given":"Jonathan","family":"Back","sequence":"additional","affiliation":[{"name":"UCL Interaction Centre, MPEB, University College London, Gower Street, WC1E 6BT, London, UK"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","volume-title":"The atomic components of thought","author":"Anderson JR","year":"1998"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1207\/s15516709cog2601_2"},{"key":"e_1_2_1_2_3_2","volume-title":"Thinking: an experimental and social study","author":"Bartlett F","year":"1958"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1207\/s15516709cog2101_2"},{"key":"e_1_2_1_2_5_2","first-page":"55","volume-title":"Formal methods and software engineering, vol 4260","author":"Beckert B","year":"2006"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-010-0129-9"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ijhcs.2012.05.010"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/s001650070021"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/s001650050045"},{"key":"e_1_2_1_2_10_2","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 Berlin pp 15\u201349","DOI":"10.1007\/978-3-642-87115-3_2"},{"key":"e_1_2_1_2_11_2","first-page":"57","volume-title":"Proceedings of the 8th IFIP working conference on engineering for human\u2013computer interaction (EHCI\u201901), vol 2254. Lecture notes in computer science","author":"Curzon P","year":"2001"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ijhcs.2007.09.001"},{"key":"e_1_2_1_2_13_2","unstructured":"Campos JC Harrison MD (2011) Modelling and analysing the interactive behaviour of an infusion pump. In: Proceedings of the fourth international workshop on formal methods for interactive systems: FMIS 2011 vol 45. Electronic communications of the EASST"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/358886.358895"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.5555\/578027"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-007-0035-6"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"de Moura L Owre S Ruess H Rushby J Shankar N Sorea M Tiwari A (2004) SAL 2. In: Alur R Peled DA (eds) Computer aided verification: CAV 2004 vol 3114. Lecture notes in computer science. Springer Berlin pp 496\u2013500","DOI":"10.1007\/978-3-540-27813-9_45"},{"key":"e_1_2_1_2_18_2","unstructured":"Fields RE (2001) Analysis of erroneous actions in the design of critical systems. Technical Report YCST 20001\/09 University of York Department of Computer Science. D.Phil Thesis"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/226650.226671"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Hudson SE John BE Knudsen K Byrne MD (1999) A tool for creating predictive performance models from user interface demonstrations. In: UIST \u201999: proceedings of the 12th annual ACM symposium on user interface software and technology. ACM Press New York pp 93\u2013102","DOI":"10.1145\/320719.322590"},{"key":"e_1_2_1_2_21_2","volume-title":"Human reliability analysis: context and control","author":"Hollnagel E","year":"1993"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1006\/imms.1993.1051"},{"key":"e_1_2_1_2_23_2","unstructured":"Huang H Ruk\u0161\u0117nas R Ament MGA Curzon P Cox AL Blandford A Brumby D (2011) Capturing the distinction between task and device errors in a formal model of user behaviour. In: Proceedings of the fourth international workshop on formal methods for interactive systems: FMIS 2011 vol 45. Electronic communications of the EASST"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/235833.236054"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/235833.236050"},{"key":"e_1_2_1_2_26_2","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 New York NY USA. ACM New York pp 455\u2013462","DOI":"10.1145\/985692.985750"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Kim BG Ayoub A Sokolsky O Lee I Jones P Zhang Y Jetley R (2011) Safety-assured development of the GPCA infusion pump software. In: Proceedings of the ninth ACM international conference on Embedded software EMSOFT \u201911 New York NY USA. ACM New York pp 155\u2013164","DOI":"10.1145\/2038642.2038667"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.1006\/ijhc.1983.0317"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/264645.264658"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Lacaze X Palanque P Navarre D Bastide R (2002) Performance evaluation as a tool for quantitative assessment of complexity of interactive systems. In: Forbrig P Limbourg Q Vanderdonckt J Urban B (eds) Interactive systems: design specification and verification vol 2545. Lecture notes in computer science. Springer Berlin pp 208\u2013222","DOI":"10.1007\/3-540-36235-5_16"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"publisher","DOI":"10.5555\/86564"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"publisher","DOI":"10.1037\/0096-1523.12.3.243"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSMC.1983.6313160"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-008-0102-7"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Ruk\u0161\u0117nas R Curzon P Back J Blandford A (2007) Formal modelling of cognitive interpretation. In: Doherty G Blandford A (eds) Interactive systems. Design specification and verification vol 4323. Lecture notes in computer science. Springer Berlin pp 123\u2013136","DOI":"10.1007\/978-3-540-69554-7_10"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80891-0"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan S Homaei H Lewis C (2011) Model-based dependability analysis of programmable drug infusion pumps. In: Fahrenberg U Tripakis S (eds) Formal modeling and analysis of timed systems vol 6919. Lecture notes in computer science. Springer Berlin pp 317\u2013334","DOI":"10.1007\/978-3-642-24310-3_22"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"Salvucci DD Lee FJ (2003) Simple cognitive modeling in a complex cognitive architecture. In: Proceedings of the SIGCHI conference on Human factors in computing systems CHI \u201903 New York NY USA. ACM New York pp 265\u2013272","DOI":"10.1145\/642611.642658"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"crossref","unstructured":"Thimbleby H (2002) Analysis and simulation of user interfaces. In: Waern Y McDonald S Cockton G (eds) Human computer interaction 2000 vol XIV. BCS conference on human\u2013computer interaction. Springer Berlin pp 221\u2013237","DOI":"10.1007\/978-1-4471-0515-2_15"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-013-0288-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-013-0288-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-013-0288-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:58:47Z","timestamp":1641484727000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-013-0288-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,9]]},"references-count":39,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2014,9]]}},"alternative-id":["10.1007\/s00165-013-0288-1"],"URL":"https:\/\/doi.org\/10.1007\/s00165-013-0288-1","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,9]]}}}