{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,30]],"date-time":"2025-12-30T23:41:49Z","timestamp":1767138109867,"version":"build-2238731810"},"publisher-location":"Cham","reference-count":32,"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_14","type":"book-chapter","created":{"date-parts":[[2017,4,24]],"date-time":"2017-04-24T04:23:43Z","timestamp":1493007823000},"page":"379-403","source":"Crossref","is-referenced-by-count":1,"title":["The Specification and Analysis of Use Properties of a Nuclear Control System"],"prefix":"10.1007","author":[{"given":"Michael D.","family":"Harrison","sequence":"first","affiliation":[]},{"given":"Paolo M.","family":"Masci","sequence":"additional","affiliation":[]},{"given":"Jos\u00e9 Creissac","family":"Campos","sequence":"additional","affiliation":[]},{"given":"Paul","family":"Curzon","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,4,25]]},"reference":[{"key":"14_CR1","unstructured":"AAMI (2010) Medical devices\u2014application of usability engineering to medical devices. Technical Report ANSI AMI IEC 62366:2007, Association for the advancement of medical instrumentation, 4301 N Fairfax Drive, Suite 301, Arlington VA 22203-1633"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"Abrial JR (2010) Modeling in event-B: system and software engineering. Cambridge University Press","DOI":"10.1017\/CBO9781139195881"},{"key":"14_CR3","doi-asserted-by":"crossref","first-page":"888","DOI":"10.1016\/j.ijhcs.2012.05.010","volume":"70","author":"ML Bolton","year":"2012","unstructured":"Bolton ML, Bass EJ, Siminiceanu RI (2012) Generating phenotypical erroneous human behavior to evaluate human-automation interaction using model checking. Int J Human-Comput Stud 70:888\u2013906","journal-title":"Int J Human-Comput Stud"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Bowen J, Reeves S (2015) Design patterns for models of interactive systems. In: 2015 24th Australasian software engineering conference (ASWEC). IEEE, pp 223\u2013232","DOI":"10.1109\/ASWEC.2015.30"},{"key":"14_CR5","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. Springer, no. 5136 in Springer lecture notes in computer science, pp 72\u201385","DOI":"10.1007\/978-3-540-70569-7_6"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Campos JC, Harrison MD (2009) Interaction engineering using the IVY tool. In: Graham T, Gray P, Calvary G (eds) Proceedings of the ACM SIGCHI symposium on engineering interactive computing systems. ACM Press, pp 35\u201344","DOI":"10.1145\/1570433.1570442"},{"key":"14_CR7","doi-asserted-by":"crossref","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"},{"issue":"2","key":"14_CR8","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1109\/THMS.2015.2421511","volume":"46","author":"JC Campos","year":"2016","unstructured":"Campos JC, Sousa M, Alves MCB, Harrison MD (2016) Formal verification of a space system\u2019s user interface with the IVY workbench. IEEE Trans Human Mach Syst 46(2):303\u2013316","journal-title":"IEEE Trans Human Mach Syst"},{"issue":"3","key":"14_CR9","first-page":"25","volume":"12","author":"DJ Duke","year":"1993","unstructured":"Duke DJ, Harrison MD (1993) Abstract interaction objects. Comput Graph. Forum 12(3):25\u201336","journal-title":"Forum"},{"key":"14_CR10","doi-asserted-by":"publisher","unstructured":"Gelman G, Feigh K, Rushby J (2013) Example of a complementary use of model checking and agent-based simulation. In: 2013 IEEE international conference on, systems, man, and cybernetics (SMC), pp 900\u2013905. doi: 10.1109\/SMC.2013.158","DOI":"10.1109\/SMC.2013.158"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Gow J, Thimbleby H, Cairns P (2006) Automatic critiques of interface modes. In: Gilroy S, Harrison M (eds) Proceedings 12th international workshop on the design, specification and verification of interactive systems. Springer, no. 3941 in Springer lecture notes in computer science, pp 201\u2013212","DOI":"10.1007\/11752707_17"},{"key":"14_CR12","unstructured":"Harrison M, Campos J, Masci P (2015a) Patterns and templates for automated verification of user interface software design in pvs. Technical report TR-1485, School of computing science, Newcastle university"},{"issue":"2","key":"14_CR13","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1007\/s11334-013-0201-3","volume":"11","author":"M Harrison","year":"2015","unstructured":"Harrison M, Campos J, Masci P (2015b) Reusing models and properties in the analysis of similar interactive devices. Innovations Syst Soft Eng 11(2):95\u2013111","journal-title":"Innovations Syst Soft Eng"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Harrison M, Campos J, Ruksenas 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"},{"key":"14_CR15","unstructured":"Harrison MD, Masci P, Campos JC, Curzon P (2014) Demonstrating that medical devices satisfy user related safety requirements. In: Proceedings of fourth symposium on foundations of health information engineering and systems (FHIES) and sixth software engineering in healthcare (SEHC) workshop. Springer, in press"},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"Heitmeyer C, Kirby J, Labaw B (1998) Applying the SRC requirements method to a weapons control panel: an experience report. In: Proceedings of the second workshop on formal methods in software practice (FMSP \u201998), pp 92\u2013102","DOI":"10.1145\/298595.298863"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"King AL, Procter S, Andresen D, Hatcliff J, Warren S, Spees W, Jetley R, Raoul P, Jones P, Weininger S (2009) An open test bed for medical device integration and coordination. In: ICSE companion, pp 141\u2013151","DOI":"10.1109\/ICSE-COMPANION.2009.5070972"},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"Konrad S, Cheng BHC (2002) Requirements patterns for embedded systems. In: Proceedings of IEEE joint international conference on requirements engineering. IEEE, pp 127\u2013136","DOI":"10.1109\/ICRE.2002.1211541"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Larson B, Hatcliff J, Procter S, Chalin P (2012) Requirements specification for apps in medical application platforms. In: Proceedings of the 4th international workshop on software engineering in health care. IEEE Press, pp 26\u201332","DOI":"10.1109\/SEHC.2012.6227013"},{"key":"14_CR20","doi-asserted-by":"crossref","unstructured":"Lavagno L, Sangiovanni-Vincentelli A, Sentovich E (1999) Models of computation for embedded system design. In: System-level synthesis. Springer, pp 45\u2013102","DOI":"10.1007\/978-94-011-4698-2_2"},{"issue":"3","key":"14_CR21","doi-asserted-by":"crossref","first-page":"642","DOI":"10.1109\/TPDS.2013.50","volume":"25","author":"T Li","year":"2014","unstructured":"Li T, Tan F, Wang Q, Bu L, Cao J, Liu X (2014) From offline toward real time: a hybrid systems model checking and CPS codesign approach for medical device plug-and-play collaborations. IEEE Trans Parallel Distrib Syst 25(3):642\u2013652","journal-title":"IEEE Trans Parallel Distrib Syst"},{"key":"14_CR22","doi-asserted-by":"publisher","unstructured":"Masci P, Huang H, Curzon P, Harrison MD (2012) Using PVS to investigate incidents through the lens of distributed cognition. In: Goodloe AE, Person S (eds) NASA formal methods, Lecture notes in computer science, vol 7226. Springer, Berlin, Heidelberg, pp 273\u2013278. doi: 10.1007\/978-3-642-28891-3_27","DOI":"10.1007\/978-3-642-28891-3_27"},{"key":"14_CR23","doi-asserted-by":"crossref","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, Ka $$\\hat{a}$$ niche M (eds) Computer safety, reliability, and security, Springer lecture notes in computer science, vol 8153. Springer, pp 228\u2013240","DOI":"10.1007\/978-3-642-40793-2_21"},{"key":"14_CR24","doi-asserted-by":"crossref","unstructured":"Masci P, Zhang Y, Jones P, Curzon P, Thimbleby HW (2014) Formal verification of medical device user interfaces using PVS. In: 17th international conference on fundamental approaches to software engineering, ETAPS\/FASE2014. Springer, Berlin, Heidelberg","DOI":"10.1007\/978-3-642-54804-8_14"},{"key":"14_CR25","doi-asserted-by":"crossref","unstructured":"Masci P, Oladimeji P, Curzon P, Thimbleby H (2015) PVSio-web 2.0: joining PVS to human-computer interaction. In: 27th international conference on computer aided verification (CAV2015). Springer, Tool and application examples available at http:\/\/www.pvsioweb.org","DOI":"10.1007\/978-3-319-21690-4_30"},{"key":"14_CR26","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"},{"issue":"5","key":"14_CR27","doi-asserted-by":"crossref","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-Mach Stud 36(5):741\u2013773","journal-title":"Int J Man-Mach Stud"},{"key":"14_CR28","unstructured":"Shankar N, Owre S, Rushby JM, Stringer-Calvert D (1999) PVS system guide, PVS language reference, PVS prover guide, PVS prelude library, abstract datatypes in PVS, and theory interpretations in PVS. Computer science laboratory, SRI international, Menlo Park, CA. http:\/\/pvs.csl.sri.com\/documentation.shtml"},{"key":"14_CR29","doi-asserted-by":"crossref","unstructured":"Sorouri M, Patil S, Vyatkin V (2012) Distributed control patterns for intelligent mechatronic systems. In: 2012 10th IEEE international conference on industrial informatics (INDIN). IEEE, pp 259\u2013264","DOI":"10.1109\/INDIN.2012.6301149"},{"key":"14_CR30","doi-asserted-by":"crossref","unstructured":"Steiner W, Rushby J (2011) TTA and PALS: formally verified design patterns for distributed cyber-physical systems. In: 2011 IEEE\/AIAA 30th digital avionics systems conference (DASC). IEEE","DOI":"10.1109\/DASC.2011.6096120"},{"issue":"10","key":"14_CR31","doi-asserted-by":"crossref","first-page":"2630","DOI":"10.1109\/TPDS.2014.2358224","volume":"26","author":"F Tan","year":"2015","unstructured":"Tan F, Wang Y, Wang Q, Bu L, Suri N (2015) A lease based hybrid design pattern for proper-temporal-embedding of wireless CPS interlocking. IEEE Trans Parallel Distrib Syst 26(10):2630\u20132642","journal-title":"IEEE Trans Parallel Distrib Syst"},{"key":"14_CR32","unstructured":"Vlissides J, Helm R, Johnson R, Gamma E (1995) Design patterns: elements of reusable object-oriented software, vol 49, no 120. Addison-Wesley, Reading, p 11"}],"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_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,21]],"date-time":"2019-09-21T14:08:26Z","timestamp":1569074906000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-51838-1_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319518374","9783319518381"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-51838-1_14","relation":{},"ISSN":["1571-5035"],"issn-type":[{"value":"1571-5035","type":"print"}],"subject":[],"published":{"date-parts":[[2017]]}}}