{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,3]],"date-time":"2025-06-03T04:14:13Z","timestamp":1748924053921,"version":"3.41.0"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319335995"},{"type":"electronic","value":"9783319336008"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-33600-8_30","type":"book-chapter","created":{"date-parts":[[2016,5,10]],"date-time":"2016-05-10T08:15:15Z","timestamp":1462868115000},"page":"344-359","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["How to Assure Correctness and Safety of Medical Software: The Hemodialysis Machine Case Study"],"prefix":"10.1007","author":[{"given":"Paolo","family":"Arcaini","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Silvia","family":"Bonfanti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Angelo","family":"Gargantini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Elvinia","family":"Riccobene","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,5,11]]},"reference":[{"key":"30_CR1","unstructured":"ISO 13485: medical devices - quality management systems - requirements for regulatory purposes (2003)"},{"key":"30_CR2","unstructured":"IEC 60601\u20131:2005 medical electrical equipment part 1: General requirements for basic safety and essential performance (2005)"},{"key":"30_CR3","doi-asserted-by":"crossref","unstructured":"IEC 62304 - medical device software - software lifecycle processes (2006)","DOI":"10.1049\/ic:20060141"},{"key":"30_CR4","unstructured":"ISO 14971: medical devices - application of risk management to medical devices (2007)"},{"key":"30_CR5","doi-asserted-by":"crossref","unstructured":"Arcaini, P., Bonfanti, S., Gargantini, A., Mashkoor, A., Riccobene, E.: Formal validation and verification of a medical software critical component. In: ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), pp. 80\u201389. IEEE, Sept 2015","DOI":"10.1109\/MEMCOD.2015.7340473"},{"key":"30_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-642-11811-1_6","volume-title":"Abstract State Machines, Alloy, B and Z","author":"P Arcaini","year":"2010","unstructured":"Arcaini, P., Gargantini, A., Riccobene, E.: AsmetaSMV: a way to link high-level ASM models to low-level NuSMV specifications. In: Frappier, M., Gl\u00e4sser, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, pp. 61\u201374. Springer, Heidelberg (2010)"},{"key":"30_CR7","unstructured":"Arcaini, P., Gargantini, A., Riccobene, E.: Automatic review of abstract state machines by meta property verification. In: Proceedings of the Second NASA Formal Methods Symposium (NFM 2010), pp. 4\u201313. NASA (2010)"},{"key":"30_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-642-29860-8_17","volume-title":"Runtime Verification","author":"P Arcaini","year":"2012","unstructured":"Arcaini, P., Gargantini, A., Riccobene, E.: CoMA: Conformance monitoring of Java programs by abstract state machines. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 223\u2013238. Springer, Heidelberg (2012)"},{"key":"30_CR9","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-319-07512-9_7","volume-title":"ABZ 2014: The Landing Gear Case Study","author":"P Arcaini","year":"2014","unstructured":"Arcaini, P., Gargantini, A., Riccobene, E.: Offline model-based testing and runtime monitoring of the sensor voting module. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. CCIS, vol. 433, pp. 95\u2013109. Springer, Heidelberg (2014)"},{"key":"30_CR10","doi-asserted-by":"crossref","unstructured":"Arcaini, P., Gargantini, A., Riccobene, E.: Rigorous development process of a safety-critical system: from ASM models to Java code. Int. J. Softw. Tools Tech. Transf., 1\u201323 (2015)","DOI":"10.1007\/s10009-015-0394-x"},{"key":"30_CR11","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1002\/spe.1019","volume":"41","author":"P Arcaini","year":"2011","unstructured":"Arcaini, P., Gargantini, A., Riccobene, E., Scandurra, P.: A model-driven process for engineering a toolset for a formal method. Softw. Pract. Experience 41, 155\u2013166 (2011)","journal-title":"Softw. Pract. Experience"},{"key":"30_CR12","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-07512-9","volume-title":"ABZ 2014: The Landing Gear Case Study","author":"F Boniol","year":"2014","unstructured":"Boniol, F., Wiels, V.: The landing gear system case study. In: Boniol, F., Wiels, V., Ameur, Y.A., Schewe, K.-D. (eds.) ABZ 2014. Communications in Computer and Information Science. Springer International Publishing, Switzerland (2014)"},{"key":"30_CR13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18216-7","volume-title":"Abstract State Machines: A Method for High-Level System Design and Analysis","author":"E B\u00f6rger","year":"2003","unstructured":"B\u00f6rger, E., St\u00e4rk, R.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003)"},{"key":"30_CR14","unstructured":"BRAUN. Dialog $$^{+^{\\textregistered }}$$ + \u00ae Dialysis Machine - Instructions for Use: Software Version 9.1x"},{"key":"30_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-540-87603-8_7","volume-title":"Abstract State Machines, B and Z","author":"A Carioni","year":"2008","unstructured":"Carioni, A., Gargantini, A., Riccobene, E., Scandurra, P.: A scenario-based validation language for ASMs. In: B\u00f6rger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 71\u201384. Springer, Heidelberg (2008)"},{"key":"30_CR16","unstructured":"EU. Directive 2007\/47\/EC of the European Parliament and of the Council. Official Journal of the European Union, September 2007"},{"key":"30_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/3-540-36498-6_15","volume-title":"Abstract State Machines 2003. Advances in Theory and Practice","author":"A Gargantini","year":"2003","unstructured":"Gargantini, A., Riccobene, E., Rinzivillo, S.: Using spin to generate testsfrom ASM specifications. In: B\u00f6rger, E., Gargantini, A., Riccobene, E. (eds.) ASM 2003. LNCS, vol. 2589, pp. 263\u2013277. Springer, Heidelberg (2003)"},{"issue":"12","key":"30_CR18","first-page":"1949","volume":"14","author":"A Gargantini","year":"2008","unstructured":"Gargantini, A., Riccobene, E., Scandurra, P.: A metamodel-based language and a simulation engine for abstract state machines. J. UCS 14(12), 1949\u20131983 (2008)","journal-title":"J. UCS"},{"issue":"4","key":"30_CR19","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1109\/MC.2006.113","volume":"39","author":"R Jetley","year":"2006","unstructured":"Jetley, R., Purushothaman Iyer, S., Jones, P.L.: A formal methods approach to medical device review. Computer 39(4), 61\u201367 (2006)","journal-title":"Computer"},{"key":"30_CR20","first-page":"329","volume-title":"Lecture Notes in Computer Science","author":"Atif Mashkoor","year":"2016","unstructured":"Mashkoor, A.: The hemodialysis machine case study. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 329\u2013343. Springer, Heidelberg (2016)"},{"key":"30_CR21","unstructured":"U.S. Food and Drug Administration (FDA). General principles of software validation; final guidance for industry and FDA staff, version 2.0, January 2002"}],"container-title":["Lecture Notes in Computer Science","Abstract State Machines, Alloy, B, TLA, VDM, and Z"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-33600-8_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,3]],"date-time":"2025-06-03T02:34:56Z","timestamp":1748918096000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-33600-8_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319335995","9783319336008"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-33600-8_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"11 May 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}