{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T16:24:38Z","timestamp":1742919878697,"version":"3.40.3"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319661964"},{"type":"electronic","value":"9783319661971"}],"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-66197-1_18","type":"book-chapter","created":{"date-parts":[[2017,8,11]],"date-time":"2017-08-11T21:02:30Z","timestamp":1502485350000},"page":"284-299","source":"Crossref","is-referenced-by-count":7,"title":["A Hazard Analysis Method for Systematic Identification of Safety Requirements for User Interface Software in Medical Devices"],"prefix":"10.1007","author":[{"given":"Paolo","family":"Masci","sequence":"first","affiliation":[]},{"given":"Yi","family":"Zhang","sequence":"additional","affiliation":[]},{"given":"Paul","family":"Jones","sequence":"additional","affiliation":[]},{"given":"Jos\u00e9 C.","family":"Campos","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,13]]},"reference":[{"unstructured":"Association for the Advancement of Medical Instrumentation: Infusing patients safely: Priority issues from the AAMI\/FDA Infusion Device Summit. AAMI (2010)","key":"18_CR1"},{"unstructured":"Blandine, A.: System Theoretic Hazard Analysis applied to the risk review of complex systems. Ph.D. thesis, MIT (2012)","key":"18_CR2"},{"issue":"12","key":"18_CR3","doi-asserted-by":"publisher","first-page":"764","DOI":"10.1177\/154193120905301201","volume":"53","author":"Matthew L Bolton","year":"2009","unstructured":"Bolton, M.L., Bass, E.J.: A method for the formal verification of human-interactive systems. In: Proceedings of the Human Factors and Ergonomics Society Annual Meeting, vol. 53(12), pp. 764\u2013768. Sage Publications (2009). doi:\n10.1177\/154193120905301201","journal-title":"Proceedings of the Human Factors and Ergonomics Society Annual Meeting"},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-319-06410-9_11","volume-title":"FM 2014: Formal Methods","author":"J Bowen","year":"2014","unstructured":"Bowen, J., Reeves, S.: A simplified Z semantics for presentation interaction models. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 148\u2013162. Springer, Cham (2014). doi:\n10.1007\/978-3-319-06410-9_11"},{"key":"18_CR5","doi-asserted-by":"publisher","DOI":"10.1002\/0471739421.ch1","volume-title":"Hazard Analysis Techniques for System Safety","author":"C Ericson","year":"2015","unstructured":"Ericson, C.: Hazard Analysis Techniques for System Safety. Wiley, New York (2015). doi:\n10.1002\/0471739421.ch1"},{"doi-asserted-by":"publisher","unstructured":"Campos, J.C., Harrison, M.D.: Interaction engineering using the IVY tool. In: EICS 2009, pp. 35\u201344. ACM (2009). doi:\n10.1145\/1570433.1570442","key":"18_CR6","DOI":"10.1145\/1570433.1570442"},{"key":"18_CR7","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-1-4471-2061-2_13","volume-title":"SAFECOMP 1993","author":"M Chudleigh","year":"1993","unstructured":"Chudleigh, M., Clare, J.N.: The benefits of SUSI: Safety analysis of user system interaction. In: G\u00f3rski, J. (ed.) SAFECOMP 1993, pp. 123\u2013132. Springer, London (1993). doi:\n10.1007\/978-1-4471-2061-2_13"},{"key":"18_CR8","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1016\/j.ssci.2013.03.013","volume":"58","author":"I Dokas","year":"2013","unstructured":"Dokas, I., Feehan, J., Imran, S.: EWaSAP: an early warning sign identification approach based on a systemic hazard analysis. Saf. Sci. 58, 11\u201326 (2013). doi:\n10.1016\/j.ssci.2013.03.013","journal-title":"Saf. Sci."},{"unstructured":"Food and Drug Administration (FDA): Class 2 Device Recall ACCUCHEK Connect Diabetes Management App (2015). \nhttps:\/\/www.accessdata.fda.gov\/scripts\/cdrh\/cfdocs\/cfRES\/res.cfm?id=134687","key":"18_CR9"},{"issue":"2","key":"18_CR10","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/s11334-013-0201-3","volume":"11","author":"MD Harrison","year":"2015","unstructured":"Harrison, M.D., Campos, J.C., Masci, P.: Reusing models and properties in the analysis of similar interactive devices. Innov. Syst. Softw. Eng. 11(2), 95\u2013111 (2015). doi:\n10.1007\/s11334-013-0201-3","journal-title":"Innov. Syst. Softw. Eng."},{"key":"18_CR11","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-319-63194-3_8","volume-title":"Lecture Notes in Computer Science","author":"Michael D. Harrison","year":"2017","unstructured":"Harrison, M.D., Masci, P., Campos, J.C., Curzon, P.: Demonstrating that medical devices satisfy user related safety requirements. In: Huhn, M., Williams, L. (eds.) Software Engineering in Health Care: 4th International Symposium, FHIES 2014, and 6th International Workshop, SEHC 2014, Washington, DC, USA, July 17\u201318, 2014, Revised Selected Papers, pp. 113\u2013128. Springer International Publishing, Cham (2017). doi:\n10.1007\/978-3-319-63194-3_8\n\n. ISBN: 978-3-319-63194-3"},{"key":"18_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1007\/3-540-40891-6_32","volume-title":"Computer Safety, Reliability and Security","author":"A Hussey","year":"2000","unstructured":"Hussey, A.: HAZOP analysis of formal models of safety-critical interactive systems. In: Koornneef, F., Meulen, M. (eds.) SAFECOMP 2000. LNCS, vol. 1943, pp. 371\u2013381. Springer, Heidelberg (2000). doi:\n10.1007\/3-540-40891-6_32"},{"unstructured":"Ishikawa, K., Lu, D.J.: What is Total Quality Control? The Japanese Way. Prentice Hall Business Classics, Prentice-Hall, Englewood Cliffs (1985)","key":"18_CR13"},{"issue":"1","key":"18_CR14","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1108\/dpm.2001.10.1.30.4","volume":"10","author":"TA Kletz","year":"2001","unstructured":"Kletz, T.A.: Hazop and hazan: identifying and assessing process industry hazards. Disaster Prev. Manage. Int. J. 10(1), 30\u201331 (2001). doi:\n10.1108\/dpm.2001.10.1.30.4","journal-title":"Disaster Prev. Manage. Int. J."},{"issue":"19","key":"18_CR15","doi-asserted-by":"publisher","first-page":"2384","DOI":"10.1001\/jama.293.19.2384","volume":"293","author":"Lucian L. Leape","year":"2005","unstructured":"Leape, L.L., Berwick, D.M.: Five years after to err is human: what have we learned? JAMA 293(19) (2005). doi:\n10.1001\/jama.293.19.2384","journal-title":"JAMA"},{"issue":"3","key":"18_CR16","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1109\/TR.1985.5222114","volume":"34","author":"WS Lee","year":"1985","unstructured":"Lee, W.S., Grosh, D.L., Tillman, F.A., Lie, C.H.: Fault tree analysis, methods, and applications: a review. IEEE Trans. Reliab. 34(3), 194\u2013203 (1985). doi:\n10.1109\/TR.1985.5222114","journal-title":"IEEE Trans. Reliab."},{"key":"18_CR17","volume-title":"Engineering a Safer World","author":"N Leveson","year":"2011","unstructured":"Leveson, N.: Engineering a Safer World. MIT Press, Cambridge (2011)"},{"key":"18_CR18","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/j.ress.2014.10.008","volume":"136","author":"N Leveson","year":"2015","unstructured":"Leveson, N.: A systems approach to risk management through leading safety indicators. Reliab. Eng. Syst. Saf. 136, 17\u201334 (2015). doi:\n10.1016\/j.ress.2014.10.008","journal-title":"Reliab. Eng. Syst. Saf."},{"key":"18_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-642-54804-8_14","volume-title":"Fundamental Approaches to Software Engineering","author":"P Masci","year":"2014","unstructured":"Masci, P., Zhang, Y., Jones, P., Curzon, P., Thimbleby, H.: Formal verification of medical device user interfaces using PVS. In: Gnesi, S., Rensink, A. (eds.) FASE 2014. LNCS, vol. 8411, pp. 200\u2013214. Springer, Heidelberg (2014). doi:\n10.1007\/978-3-642-54804-8_14"},{"doi-asserted-by":"publisher","unstructured":"Masci, P., Ayoub, A., Curzon, P., Harrison, M.D., Lee, I., Thimbleby, H.: Verification of interactive software for medical devices: PCA infusion pumps and FDA Regulation as an example. In: EICS 2013, pp. 81\u201390. ACM (2013). doi:\n10.1145\/2494603.2480302","key":"18_CR20","DOI":"10.1145\/2494603.2480302"},{"issue":"2","key":"18_CR21","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.: Using PVS to support the analysis of distributed cognition systems. Innov. Syst. Softw. Eng. 11(2), 113\u2013130 (2015). doi:\n10.1007\/s11334-013-0202-2","journal-title":"Innov. Syst. Softw. Eng."},{"key":"18_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-642-33176-3_11","volume-title":"Software Engineering for Resilient Systems","author":"P Masci","year":"2012","unstructured":"Masci, P., Furniss, D., Curzon, P., Harrison, M.D., Blandford, A.: Supporting field investigators with PVS: a case study in the healthcare domain. In: Avgeriou, P. (ed.) SERENE 2012. LNCS, vol. 7527, pp. 150\u2013164. Springer, Heidelberg (2012). doi:\n10.1007\/978-3-642-33176-3_11"},{"key":"18_CR23","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-08-052029-2.50001-2","volume-title":"Usability Engineering","author":"J Nielsen","year":"1993","unstructured":"Nielsen, J.: Usability Engineering. Morgan Kaufmann, San Francisco (1993). doi:\n10.1016\/B978-0-08-052029-2.50001-2"},{"key":"18_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction\u2014CADE-11","author":"S Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748\u2013752. Springer, Heidelberg (1992). doi:\n10.1007\/3-540-55602-8_217"},{"issue":"2","key":"18_CR25","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/s11334-013-0200-4","volume":"11","author":"P Masci","year":"2015","unstructured":"Masci, P., Ruk\u0161\u0117nas, R., Oladimeji, P., Cauchi, A., Gimblett, A., Li, Y., Curzon, P., Thimbleby, H.: The benefits of formalising design guidelines: a case study on the predictability of drug infusion pumps. Innov. Syst. Softw. Eng. 11(2), 73\u201393 (2015). doi:\n10.1007\/s11334-013-0200-4","journal-title":"Innov. Syst. Softw. Eng."},{"key":"18_CR26","series-title":"IFIP \u2014 The International Federation for Information Processing","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1007\/978-0-387-35175-9_58","volume-title":"Human-Computer Interaction INTERACT \u201997","author":"F Paterno","year":"1997","unstructured":"Paterno, F., Mancini, C., Meniconi, S.: ConcurTaskTrees: a diagrammatic notation for specifying task models. In: Howard, S., Hammond, J., Lindgaard, G. (eds.) Human-Computer Interaction INTERACT \u201997. ITIFIP, pp. 362\u2013369. Springer, Boston, MA (1997). doi:\n10.1007\/978-0-387-35175-9_58"},{"doi-asserted-by":"publisher","unstructured":"Procter, S., Hatcliff, J.: An architecturally-integrated, systems-based hazard analysis for medical applications. In: MEMOCODE 2014, pp. 124\u2013133. IEEE (2014). doi:\n10.1109\/MEMCOD.2014.6961850","key":"18_CR27","DOI":"10.1109\/MEMCOD.2014.6961850"},{"key":"18_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-540-69554-7_10","volume-title":"Interactive Systems. Design, Specification, and Verification","author":"R Ruk\u0161\u0117nas","year":"2007","unstructured":"Ruk\u0161\u0117nas, R., Curzon, P., Back, J., Blandford, A.: Formal modelling of cognitive interpretation. In: Doherty, G., Blandford, A. (eds.) DSV-IS 2006. LNCS, vol. 4323, pp. 123\u2013136. Springer, Heidelberg (2007). doi:\n10.1007\/978-3-540-69554-7_10"},{"issue":"2","key":"18_CR29","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1016\/S0951-8320(01)00092-8","volume":"75","author":"J Rushby","year":"2002","unstructured":"Rushby, J.: Using model checking to help discover mode confusions and other automation surprises. Reliab. Eng. Syst. Saf. 75(2), 167\u2013177 (2002). doi:\n10.1016\/S0951-8320(01)00092-8","journal-title":"Reliab. Eng. Syst. Saf."},{"key":"18_CR30","volume-title":"Failure Mode And Effect Analysis","author":"D Stamatis","year":"2003","unstructured":"Stamatis, D.: Failure Mode And Effect Analysis. ASQ Quality Press, Milwaukee (2003)"},{"unstructured":"Thornberry, C.: Extending the human-controller methodology in systems-theoretic process analysis (STPA). Ph.D. thesis, MIT (2014)","key":"18_CR31"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66197-1_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,7,24]],"date-time":"2018-07-24T23:53:18Z","timestamp":1532476398000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66197-1_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319661964","9783319661971"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66197-1_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}