{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:36:54Z","timestamp":1761597414724},"reference-count":42,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2013,4,3]],"date-time":"2013-04-03T00:00:00Z","timestamp":1364947200000},"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-0201-3","type":"journal-article","created":{"date-parts":[[2013,4,2]],"date-time":"2013-04-02T10:41:27Z","timestamp":1364899287000},"page":"95-111","source":"Crossref","is-referenced-by-count":21,"title":["Reusing models and properties in the analysis of similar interactive devices"],"prefix":"10.1007","volume":"11","author":[{"given":"Michael D.","family":"Harrison","sequence":"first","affiliation":[]},{"given":"Jos\u00e9 Creissac","family":"Campos","sequence":"additional","affiliation":[]},{"given":"Paolo","family":"Masci","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2013,4,3]]},"reference":[{"key":"201_CR1","doi-asserted-by":"crossref","unstructured":"Amnell T, Behrmann G, Bengtsson J, D\u2019Argenio PR, David A, Fehnker A, Hune T, Jeannet B, Larsen KG, M\u00f6ller MO, Pettersson P, Weise C, Yi W (2001) UPPAAL-Now, Next, and Future. In: Cassez F, Jard C, Rozoy B, Ryan M (eds) Modelling and Verification of Parallel Processes, number 2067 in Lecture Notes in Computer Science Tutorial, Springer-Verlag, Berlin, pp 100\u2013125","DOI":"10.1007\/3-540-45510-8_4"},{"key":"201_CR2","unstructured":"Arney D, Kim B, Jetley R, Jones P, Lee I, Ray A, Sokolsky O, Zhang Y (0000) Safety requirements for the generic patient controlled analgesia pump. http:\/\/rtg.cis.upenn.edu\/gip.php3"},{"key":"201_CR3","unstructured":"B. Braun Melsungen AG (2007) B.Braun Infusomat Space User Manual. Technical report, B. Braun Melsungen AG, 34209 Melsungen, Germany"},{"key":"201_CR4","doi-asserted-by":"crossref","unstructured":"Bligard L-A, Osvalder A-L (2007) An analytical approach for predicting and identifying use error and usability problem. In: Holzinger A (ed) Proceedings of the 3rd Human-computer interaction and usability engineering of the Austrian computer society conference on HCI and usability for medicine and health care, number 4799 in Springer Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp 427\u2013440","DOI":"10.1007\/978-3-540-76805-0_38"},{"issue":"3","key":"201_CR5","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1007\/s11334-010-0129-9","volume":"6","author":"ML Bolton","year":"2010","unstructured":"Bolton ML, Bass EJ (2010) Formally verifying human-automation interaction as part of a system model: limitations and tradeoffs. Innov Syst Softw Eng 6(3):219\u2013231","journal-title":"Innov Syst Softw Eng"},{"key":"201_CR6","doi-asserted-by":"crossref","unstructured":"Bolton ML, Bass EJ, Sininiceanu RI (2012) Generating phenotypical erroneous human behavior to evaluate human-automation interaction using model checking. Intern J Hum Comput Stud 70: 888\u2013906","DOI":"10.1016\/j.ijhcs.2012.05.010"},{"key":"201_CR7","doi-asserted-by":"crossref","unstructured":"Bolton ML, Bass EJ, Siminiceanu RI (2013) Using formal verification to evaluate human-automation interaction, a review. IEEE Transactions on Systems, Man, and Cybernetics, Part A: Systems and Humans 99:1\u201316","DOI":"10.1109\/TSMCA.2012.2210406"},{"key":"201_CR8","unstructured":"Campos JC (2012) Minho HCI repository. http:\/\/hcispecs.di.uminho.pt"},{"key":"201_CR9","doi-asserted-by":"crossref","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":"201_CR10","doi-asserted-by":"crossref","unstructured":"Campos JC, Harrison MD (2008) Systematic analysis of control panel interfaces using formal tools. In: Graham N, Palanque P (eds) Interactive systems: Design, Specification and Verification, DSVIS \u201908, number 5136 in Springer Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp 72\u201385","DOI":"10.1007\/978-3-540-70569-7_6"},{"key":"201_CR11","doi-asserted-by":"crossref","unstructured":"Campos JC, Harrison MD (2009) Interaction engineering using the IVY tool. In: Calvary G, Graham TCN, Gray P (eds) Proceedings of the ACM SIGCHI Symposium on Engineering Interactive Computing Systems, ACM Press, New York, pp 35\u201344","DOI":"10.1145\/1570433.1570442"},{"key":"201_CR12","unstructured":"Campos JC, Harrison MD (2011) Modelling and analysing the interactive behaviour of an infusion pump. Electronic Communications of the EASST, 5, San Ramon"},{"key":"201_CR13","unstructured":"Campos JC, Harrison MD (1997) Formally Verifying Interactive Systems: A Review. In: Harrison MD, Torres JC (eds) Proceedings on the 4th Eurographics Workshop on Design, Specification and Verification of Interactive Systems (DSVIS), Springer-Verlag, Berlin, pp 119\u2013134"},{"key":"201_CR14","unstructured":"Cardinal Health Inc (2006) Alaris GP volumetric pump: directions for use. Technical report, Cardinal Health, 1180 Rolle, Switzerland"},{"key":"201_CR15","doi-asserted-by":"crossref","unstructured":"Cimatti A, Clarke E, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, Tacchella A (2002) NuSMV 2: An Open Source Tool for Symbolic Model Checking. In: Larsen KG, Brinksma E (eds) Computer-Aided Verification (CAV \u201902), vol 2404, Lecture Notes in Computer Science, Springer-Verlag, Berlin","DOI":"10.1007\/3-540-45657-0_29"},{"key":"201_CR16","unstructured":"Clarke EM, Grumberg O, Peled DA (1999) Model Checking. MIT Press, Cambridge"},{"key":"201_CR17","unstructured":"Moura de L (2004) SAL: Tutorial. Technical report, SRI International. Computer Science Laboratory, 333 Ravenswood Avenue, Menlo Park"},{"key":"201_CR18","unstructured":"Dix A, Finlay J, Abowd G, Beale R (1993) Human-Computer Interaction. ACM SIGCHI Bulletin, Prentice Hall"},{"key":"201_CR19","unstructured":"Dix AJ (1991) Formal Methods for Interactive Systems. Academic Press, London"},{"key":"201_CR20","doi-asserted-by":"crossref","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, vol 5136. Springer Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp 194\u2013207","DOI":"10.1007\/978-3-540-70569-7_19"},{"issue":"3","key":"201_CR21","doi-asserted-by":"crossref","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 Gr Forum 12(3):25\u201336","journal-title":"Comput Gr Forum"},{"key":"201_CR22","doi-asserted-by":"crossref","unstructured":"Fiadeiro J, Maibaum T, Bakker de J, Roever de W, Rozenberg G (1991) Describing, structuring and implementing objects. In: Foundations of Object-Oriented Languages, number 489 in Springer Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp 274\u2013310","DOI":"10.1007\/BFb0019447"},{"key":"201_CR23","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"},{"key":"201_CR24","unstructured":"US Food and Drug Administration (2010) Infusion pump improvement initiative. Technical report, Center for Devices and Radiological Health. University of York, New york"},{"issue":"2","key":"201_CR25","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1518\/001872007X312522","volume":"49","author":"M Heymann","year":"2007","unstructured":"Heymann M, Degani A (2007) Formal analysis and automatic generation of user interfaces: approach, methodology, and an algorithm. J Hum Fact Ergon Soc 49(2):311\u2013330","journal-title":"J Hum Fact Ergon Soc"},{"key":"201_CR26","unstructured":"Johnson-Laird PN (1983) Mental Models. Harvard University Press, Cambridge"},{"key":"201_CR27","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 9th ACM international conference on Embedded software, EMSOFT \u201911, ACM, New York, pp 155\u2013164","DOI":"10.1145\/2038642.2038667"},{"key":"201_CR28","doi-asserted-by":"crossref","unstructured":"Kirwan B, Ainsworth L (1992) A Guide to Task Analysis. Taylor and Francis, Lodon","DOI":"10.1201\/b16826"},{"key":"201_CR29","doi-asserted-by":"crossref","first-page":"669","DOI":"10.1016\/j.apergo.2005.08.001","volume":"37","author":"R Lane","year":"2006","unstructured":"Lane R, Stanton NA, Harrison D (2006) Applying hierarchical task analysis to medication administration errors. Appl Ergon 37:669\u2013679","journal-title":"Appl Ergon"},{"issue":"1\u2014-2","key":"201_CR30","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen KG, Pettersson P, Yi W (1997) UPPAAL in a Nutshell. Int J Softw Tool Technol Transf 1(1\u2014-2):134\u2013152","journal-title":"Int J Softw Tool Technol Transf"},{"key":"201_CR31","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, vol 45. ECEASST, Bolton"},{"key":"201_CR32","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, New York, pp 249\u2013256","DOI":"10.1145\/97243.97281"},{"key":"201_CR33","unstructured":"Oladimeji P (2012) Alaris simulation. http:\/\/cs.swan.ac.uk\/cspo\/simulations"},{"key":"201_CR34","doi-asserted-by":"crossref","unstructured":"Oladimeji P, Thimbleby H, Cox A (2011) Number entry and their effects on error detection. In: Campos P et al (eds) Interact 2011, number 6949 in Springer Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp 178\u2013185","DOI":"10.1007\/978-3-642-23768-3_15"},{"key":"201_CR35","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 \u201992 Conference, Cambridge University Press, BCS HCI Specialist Group, Cambridge, pp 155\u2013174"},{"key":"201_CR36","doi-asserted-by":"crossref","unstructured":"Ruksenas R, Back J, Curzon P, Blandford A (2009) Verification-guided modelling of salience and cognitive load. Form Asp Comput 21:541\u2013569","DOI":"10.1007\/s00165-008-0102-7"},{"key":"201_CR37","doi-asserted-by":"crossref","unstructured":"Ryan M, Fiadeiro J, Maibaum T (1991) Sharing actions and attributes in modal action logic. In Theoretical Aspects of Computer Software, volume 526 of Springer Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp 569\u2013593","DOI":"10.1007\/3-540-54415-1_65"},{"issue":"51","key":"201_CR38","doi-asserted-by":"crossref","first-page":"1429","DOI":"10.1098\/rsif.2010.0112","volume":"7","author":"H Thimbleby","year":"2010","unstructured":"Thimbleby H, Cairns P (2010) Reducing number entry errors: solving a widespread, serious problem. J R Soc Interf 7(51):1429\u20131439","journal-title":"J R Soc Interf"},{"key":"201_CR39","unstructured":"Thimbleby H, Gimblett A (2011) Dependable keyed data entry for interactive systems, vol 45. ECEASST, Bolton"},{"key":"201_CR40","doi-asserted-by":"crossref","unstructured":"Thimbleby H (2007) Interaction walkthrough: evaluation of safety critical interactive systems. In: Doherty G, Blandford A (eds Interactive Systems: Design, Specification and Verification, number 4323 in Springer Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp 52\u201366","DOI":"10.1007\/978-3-540-69554-7_5"},{"key":"201_CR41","unstructured":"Thimbleby H (2007) Press on: principles of interaction programming. MIT Press, Cambridge"},{"key":"201_CR42","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1016\/S1532-0464(03)00060-1","volume":"36","author":"J Zhang","year":"2003","unstructured":"Zhang J, Johnson TR, Patel VL, Paige DL, Kuboseb T (2003) Using usability heuristics to evaluate patient safety of medical devices. J Biomed Inform 36:23\u201330","journal-title":"J Biomed Inform"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-013-0201-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11334-013-0201-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-013-0201-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,11]],"date-time":"2019-07-11T17:18:58Z","timestamp":1562865538000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11334-013-0201-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,4,3]]},"references-count":42,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2015,6]]}},"alternative-id":["201"],"URL":"https:\/\/doi.org\/10.1007\/s11334-013-0201-3","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,4,3]]}}}