{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:49:18Z","timestamp":1740098958890,"version":"3.37.3"},"publisher-location":"Cham","reference-count":17,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319680330"},{"type":"electronic","value":"9783319680347"}],"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-68034-7_8","type":"book-chapter","created":{"date-parts":[[2017,9,13]],"date-time":"2017-09-13T13:32:45Z","timestamp":1505309565000},"page":"137-154","source":"Crossref","is-referenced-by-count":4,"title":["Safety Analysis of Software Components of a Dialysis Machine Using Model Checking"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5567-9650","authenticated-orcid":false,"given":"M. D.","family":"Harrison","sequence":"first","affiliation":[]},{"given":"M.","family":"Drinnan","sequence":"additional","affiliation":[]},{"given":"J. C.","family":"Campos","sequence":"additional","affiliation":[]},{"given":"P.","family":"Masci","sequence":"additional","affiliation":[]},{"given":"L.","family":"Freitas","sequence":"additional","affiliation":[]},{"given":"C.","family":"di Maria","sequence":"additional","affiliation":[]},{"given":"M.","family":"Whitaker","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,9,14]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"J-R Abrial","year":"2010","unstructured":"Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, New York (2010)"},{"issue":"1","key":"8_CR2","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1109\/32.210305","volume":"19","author":"JM Atlee","year":"1993","unstructured":"Atlee, J.M., Gannon, J.: State-based model checking of event-driven system requirements. IEEE Trans. Softw. Eng. 19(1), 24\u201340 (1993)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"8_CR3","unstructured":"Barnes, J., Chapman, R., Johnson, R., Everett, B., Cooper, D.: Engineering the tokeneer enclave protection software. In: IEEE International Symposium on Secure Software Engineering. IEEE (2006)"},{"key":"8_CR4","unstructured":"BSI: Medical device software - software life cycle processes. Technical report BS EN 62304:2006, British Standards Institution, CENELEC, Avenue Marnix 17, B-1000 Brussels (2008)"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/978-3-540-70569-7_6","volume-title":"Interactive Systems. Design, Specification, and Verification","author":"JC Campos","year":"2008","unstructured":"Campos, J.C., Harrison, M.D.: Systematic analysis of control panel interfaces using formal tools. In: Graham, T.C.N., Palanque, P. (eds.) DSV-IS 2008. LNCS, vol. 5136, pp. 72\u201385. Springer, Heidelberg (2008). doi:\n10.1007\/978-3-540-70569-7_6"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359\u2013364. Springer, Heidelberg (2002). doi:\n10.1007\/3-540-45657-0_29"},{"key":"8_CR7","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"8_CR8","unstructured":"Freitas, L., Stabler, A.: Translation strategies for medical device control software. Technical report, Newcastle University, August 2015"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/978-3-319-63194-3_8","volume-title":"Software Engineering in Health Care","author":"MD 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.) FHIES 2014. LNCS, vol. 9062, pp. 113\u2013128. Springer International Publishing, Cham (2017)"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"526","DOI":"10.1007\/BFb0028775","volume-title":"Computer Aided Verification","author":"C Heitmeyer","year":"1998","unstructured":"Heitmeyer, C., Kirby, J., Labaw, B., Bharadwaj, R.: SCR: a toolset for specifying and analyzing software requirements. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 526\u2013531. Springer, Heidelberg (1998). doi:\n10.1007\/BFb0028775"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/978-3-540-45236-2_4","volume-title":"FME 2003: Formal Methods","author":"GJ Holzmann","year":"2003","unstructured":"Holzmann, G.J.: Trends in software verification. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 40\u201350. Springer, Heidelberg (2003). doi:\n10.1007\/978-3-540-45236-2_4"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Kim, B., Ayoub, A., Sokolsky, O., Lee, I., Jones, P., Zhang, Y., Jetley, R.: Safety-assured development of the GPCA infusion pump software. In: Proceedings of the Ninth ACM International Conference on Embedded software, EMSOFT 2011, pp. 155\u2013164. ACM, New York (2011)","DOI":"10.1145\/2038642.2038667"},{"issue":"1","key":"8_CR13","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1145\/2560537","volume":"32","author":"G Klein","year":"2014","unstructured":"Klein, G., Andronick, J., Elphinstone, K., Murray, T.C., Sewell, T., Kolanski, R., Heiser, G.: Comprehensive formal verification of an OS microkernel. ACM Trans. Comput. Syst. 32(1), 2 (2014)","journal-title":"ACM Trans. Comput. Syst."},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Masci, P., Ayoub, A., Curzon, P., Harrison, M.D., Lee, I., Sokolsky, O., Thimbleby, H.: Verification of interactive software for medical devices: PCA infusion pumps and FDA regulation as an example. In: Proceedings ACM Symposium Engineering Interactive Systems (EICS 2013), pp. 81\u201390. ACM Press (2013)","DOI":"10.1145\/2494603.2480302"},{"key":"8_CR15","first-page":"185","volume-title":"User-Centred Requirements For Software Engineering","author":"AF Monk","year":"1991","unstructured":"Monk, A.F., Curry, M., Wright, P.C.: Why industry doesn\u2019t use the wonderful notations we researchers have given them to reason about their designs. In: Gilmore, D.J., Winder, R.L., Detienne, F. (eds.) User-Centred Requirements For Software Engineering, pp. 185\u2013189. Springer, Berlin, Heidelberg (1991)"},{"key":"8_CR16","unstructured":"US Food and Drug Administration: General principles of software validation: final guidance for industry and FDA staff. Technical report, Center for Devices and Radiological Health, January 2002. \nhttp:\/\/www.fda.gov\/medicaldevices\/deviceregulationandguidance"},{"key":"8_CR17","unstructured":"Yeganefard, S., Butler, M.: Structuring functional requirements of control systems to facilitate refinement-based formalisation. In: Proceedings of the 11th International Workshop on Automated Verification of Critical Systems (AVoCS 2011), vol. 46. Electronic Communications of the EASST (2011)"}],"container-title":["Lecture Notes in Computer Science","Formal Aspects of Component Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-68034-7_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,9,13]],"date-time":"2017-09-13T13:35:01Z","timestamp":1505309701000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-68034-7_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319680330","9783319680347"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-68034-7_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}