{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,12]],"date-time":"2023-09-12T00:23:29Z","timestamp":1694478209570},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2013,4,2]],"date-time":"2013-04-02T00:00:00Z","timestamp":1364860800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2015,6]]},"DOI":"10.1007\/s11334-013-0200-4","type":"journal-article","created":{"date-parts":[[2013,4,1]],"date-time":"2013-04-01T11:41:39Z","timestamp":1364816499000},"page":"73-93","source":"Crossref","is-referenced-by-count":20,"title":["The benefits of formalising design guidelines: a case study on the predictability of drug infusion pumps"],"prefix":"10.1007","volume":"11","author":[{"given":"Paolo","family":"Masci","sequence":"first","affiliation":[]},{"given":"Rimvydas","family":"Ruk\u0161\u0117nas","sequence":"additional","affiliation":[]},{"given":"Patrick","family":"Oladimeji","sequence":"additional","affiliation":[]},{"given":"Abigail","family":"Cauchi","sequence":"additional","affiliation":[]},{"given":"Andy","family":"Gimblett","sequence":"additional","affiliation":[]},{"given":"Yunqiu","family":"Li","sequence":"additional","affiliation":[]},{"given":"Paul","family":"Curzon","sequence":"additional","affiliation":[]},{"given":"Harold","family":"Thimbleby","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2013,4,2]]},"reference":[{"key":"200_CR1","unstructured":"List of errorprone abbreviations, symbols and dose designations (2006). http:\/\/www.ismp.org\/tools\/abbreviations\/"},{"key":"200_CR2","doi-asserted-by":"crossref","unstructured":"Arney D, Jetley R, Jones P, Lee I, Sokolsky O (2007) Formal methods based development of a PCA infusion pump reference model: generic infusion pump (GIP) project. In: Joint Workshop on High Confidence Medical Devices, Software, and Systems and Medical Device Plug-and-Play Interoperability 0, pp 23\u201333. doi: 10.1109\/HCMDSS-MDPnP.2007.36","DOI":"10.1109\/HCMDSS-MDPnP.2007.36"},{"key":"200_CR3","unstructured":"B-Braun Melsungen AG: Infusomat space and accessory: Instruction for use"},{"key":"200_CR4","doi-asserted-by":"crossref","unstructured":"Back J, Brumby DP, Cox AL (2010) Locked-out: investigating the effectiveness of system lockouts to reduce errors in routine tasks. In: Proceedings of the 28th of the international conference extended abstracts on Human factors in computing systems, CHI EA \u201910. ACM, New York, pp 3775\u20133780. doi: 10.1145\/1753846.1754054","DOI":"10.1145\/1753846.1754054"},{"key":"200_CR5","unstructured":"Bass EJ, Feigh KM, Gunter EL, Rushby JM (2011) Formal modeling and analysis for interactive hybrid systems. ECEASST 45"},{"key":"200_CR6","unstructured":"Bolton ML, Bass EJ (2010) Formally verifying human\u2013automation interaction as part of a system model: limitations and tradeoffs. Innov Syst Softw Eng 6(3):219\u2013231. doi: 10.1007\/s11334-010-19730129-9"},{"key":"200_CR7","doi-asserted-by":"crossref","unstructured":"Campos JC, Harrison MD (2009) Interaction engineering using the ivy tool. In: Proceedings of the 1st ACM SIGCHI symposium on Engineering interactive computing systems, EICS \u201909. ACM, New York, pp 35\u201344. doi: 10.1145\/1570433.1570442","DOI":"10.1145\/1570433.1570442"},{"key":"200_CR8","unstructured":"Campos JC, Harrison MD (2011) Modelling and analysing the interactive behaviour of an infusion pump. ECEASST 45"},{"key":"200_CR9","doi-asserted-by":"crossref","unstructured":"Cauchi A, Gimblett A, Thimbleby A, Curzon P, Masci P (2012) Safer \u201c5-key\u201d number entry user interfaces using differential formal analysis. In: 26th Annual Conference on Human\u2013Computer Interaction, BCS-HCI","DOI":"10.1145\/2305484.2305540"},{"issue":"1","key":"200_CR10","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1518\/0018720024494838","volume":"44","author":"A Degani","year":"2002","unstructured":"Degani A, Heymann M (2002) Formal verification of human\u2013automation interaction. Human Factors 44(1):28\u201343","journal-title":"Human Factors"},{"key":"200_CR11","unstructured":"Department fo Health and Human Services, US Food and Drug Administration (2010) Total Product Life Cycle: Infusion Pump\u2014Premarket Notification [510(k)] Submissions\u2014Draft Guidance, April 2010"},{"key":"200_CR12","unstructured":"Dix AJ (1991) Formal methods for interactive systems. Computers and people series. Academic Press, San Diego. http:\/\/www.hiraeth.com\/books\/formal\/"},{"key":"200_CR13","unstructured":"Dix AJ, Runciman C (1985) Abstract models of interactive systems. People and computers: designing the interface. Cambridge University Press, Cambridge, pp 13\u201322"},{"key":"200_CR14","unstructured":"Harrison MD, Thimbleby H (1985)Abstract models of interactive systems. In: Proceedings British Computer Society Conference on Human Computer Interaction (HCI\u201985). Cambridge University Press, Cambridge, pp 161\u2013171"},{"key":"200_CR15","doi-asserted-by":"crossref","unstructured":"Endsley MR, Bolte B, Jones DG (2003) Designing for situation awareness: an approach to user-centered design. Taylor and Francis, Boca Raton","DOI":"10.1201\/9780203485088"},{"key":"200_CR16","unstructured":"Health C (2006) Alaris GP volumetric pump: directions for use"},{"key":"200_CR17","doi-asserted-by":"crossref","unstructured":"Hinckley K, Cutrell E, Bathiche S, Muss T (2002) Quantitative analysis of scrolling techniques. In: Proceedings of the SIGCHI conference on Human factors in computing systems: changing our world, changing ourselves, CHI \u201902. ACM, New York, pp 65\u201372. doi: 10.1145\/503376.503389","DOI":"10.1145\/503376.503389"},{"key":"200_CR18","unstructured":"Javaux D (1998) Explaining sarter and woods\u2019 classical results. In: Second Workshop on Human Error, Safety, and Software Design"},{"key":"200_CR19","doi-asserted-by":"crossref","unstructured":"Kim B, 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. ACM, New York, pp 155\u2013164. doi: 10.1145\/2038642.2038667","DOI":"10.1145\/2038642.2038667"},{"issue":"23","key":"200_CR20","doi-asserted-by":"crossref","first-page":"1851","DOI":"10.1001\/jama.1994.03520230061039","volume":"272","author":"L Leape","year":"1994","unstructured":"Leape L (1994) Error in medicine. J Am Med Assoc 272(23):1851\u20131857","journal-title":"J Am Med Assoc"},{"key":"200_CR21","unstructured":"Masci P, Ruk\u0161\u0117nas R, Oladimeji P, Cauchi A, Gimblett A, Li Y, Curzon P, Thimbleby H (2011) On formalising interactive number entry on infusion pumps. ECEASST"},{"key":"200_CR22","unstructured":"Medicines and Healthcare products Regulatory Agency (MHRA) (2010) Device bulletin, infusion systems, db2003(02) v2.0. http:\/\/www.mhra.gov.uk\/Publications\/Safetyguidance\/DeviceBulletins\/CON007321"},{"key":"200_CR23","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, Lecture Notes in Computer Science, vol 3114. Springer, Berlin, pp 496\u2013500","DOI":"10.1007\/978-3-540-27813-9_45"},{"key":"200_CR24","doi-asserted-by":"crossref","unstructured":"Norman DA (1983) Design rules based on analyses of human error. Commun ACM 26(4):254\u2013258. doi: 10.1145\/2163.358092","DOI":"10.1145\/2163.358092"},{"key":"200_CR25","unstructured":"Norman DA (2002) The Design of Everyday Things, reprint paperback edn. Basic Books, New York"},{"key":"200_CR26","doi-asserted-by":"crossref","unstructured":"Oladimeji P, Thimbleby H, Cox A (2011) Number entry interfaces and their effects on error detection. In: Proceedings of the 13th IFIP TC 13 international conference on Human\u2013computer interaction\u2014Volume Part IV, INTERACT\u201911. Springer, Berlin, pp 178\u2013185. http:\/\/dl.acm.org\/citation.cfm?id=2042283.2042302","DOI":"10.1007\/978-3-642-23768-3_15"},{"key":"200_CR27","volume-title":"Normal accidents: living with high-risk technologies","author":"C Perrow","year":"1984","unstructured":"Perrow C (1984) Normal accidents: living with high-risk technologies. Basic Books, New York"},{"key":"200_CR28","doi-asserted-by":"crossref","unstructured":"Reason J (1990) Human error, 1st edn. Cambridge University Press, Cambridge","DOI":"10.1017\/CBO9781139062367"},{"key":"200_CR29","doi-asserted-by":"crossref","unstructured":"Rushby J (2002) Using model checking to help discover mode confusions and other automation surprises. Reliab Eng System Safety 75(2):167\u2013177. http:\/\/www.csl.sri.com\/users\/rushby\/abstracts\/ress02","DOI":"10.1016\/S0951-8320(01)00092-8"},{"key":"200_CR30","doi-asserted-by":"crossref","unstructured":"Rushby JM (2001) Modeling the human in human factors. In: Proceedings of the 20th International Conference on Computer Safety, Reliability and Security, SAFECOMP \u201901. Springer, London, pp 86\u201391. http:\/\/dl.acm.org\/citation.cfm?id=647399.724851","DOI":"10.1007\/3-540-45416-0_9"},{"key":"200_CR31","doi-asserted-by":"crossref","unstructured":"Ryan M, Fiadeiro JL, Maibaum TSE (1991) Sharing actions and attributes in modal action logic. In: TACS, pp 569\u2013593","DOI":"10.1007\/3-540-54415-1_65"},{"issue":"3","key":"200_CR32","doi-asserted-by":"crossref","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 Human Comput Studies 54(3):333\u2013350. doi: 10.1006\/ijhc.2000.0442","journal-title":"Int J Human Comput Studies"},{"key":"200_CR33","doi-asserted-by":"crossref","unstructured":"Thimbleby H (2007) Interaction walkthrough: evaluation of safety critical interactive systems. In: Doherty G, Blandford A (eds) DSVIS 2006, The XIII International Workshop on Design, Specification and Verification of Interactive Systems, Lecture Notes in Computer Science, vol 4323. Springer, Berlin, pp 52\u201366","DOI":"10.1007\/978-3-540-69554-7_5"},{"key":"200_CR34","unstructured":"Thimbleby HW, Gimblett A (2011) Dependable keyed data entry for interactive systems. ECEASST 45"},{"key":"200_CR35","doi-asserted-by":"crossref","unstructured":"Trafton GJ, Monk CA (2007) Task interruptions. Rev Human Factors Ergonomics. 3(16):111\u2013126. doi: 10.1518\/155723408X299852 . http:\/\/www.ingentaconnect.com\/content\/hfes\/rhfe\/2007\/00000003","DOI":"10.1518\/155723408X299852"},{"key":"200_CR36","doi-asserted-by":"crossref","unstructured":"Vincent (2011) Patient safety, 2nd edn. Wiley, New York","DOI":"10.1002\/9781444323856"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-013-0200-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11334-013-0200-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-013-0200-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,24]],"date-time":"2020-07-24T17:02:01Z","timestamp":1595610121000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11334-013-0200-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,4,2]]},"references-count":36,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2015,6]]}},"alternative-id":["200"],"URL":"https:\/\/doi.org\/10.1007\/s11334-013-0200-4","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,4,2]]}}}