{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:50:43Z","timestamp":1725936643941},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319731162"},{"type":"electronic","value":"9783319731179"}],"license":[{"start":{"date-parts":[[2017,12,22]],"date-time":"2017-12-22T00:00:00Z","timestamp":1513900800000},"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":[[2018]]},"DOI":"10.1007\/978-3-319-73117-9_17","type":"book-chapter","created":{"date-parts":[[2017,12,21]],"date-time":"2017-12-21T16:45:34Z","timestamp":1513874734000},"page":"241-254","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Formal Verification and Safety Assessment of\u00a0a\u00a0Hemodialysis Machine"],"prefix":"10.1007","author":[{"given":"Shahid","family":"Khan","sequence":"first","affiliation":[]},{"given":"Osman","family":"Hasan","sequence":"additional","affiliation":[]},{"given":"Atif","family":"Mashkoor","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,12,22]]},"reference":[{"key":"17_CR1","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-319-20615-8_3","volume-title":"Intelligent Computer Mathematics","author":"W Ahmed","year":"2015","unstructured":"Ahmed, W., Hasan, O.: Towards formal fault tree analysis using theorem proving. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS (LNAI), vol. 9150, pp. 39\u201354. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-20615-8_3"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"Arcaini, P., Bonfanti, S., Gargantini, A., Mashkoor, A., Riccobene, E.: Integrating formal methods into medical software development: the ASM approach. Sci. Comput. Program. (2017, in press)","DOI":"10.1016\/j.scico.2017.07.003"},{"key":"17_CR3","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P., Larsen, K.G.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"17_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1007\/978-3-319-33600-8_32","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"R Banach","year":"2016","unstructured":"Banach, R.: Hemodialysis machine in hybrid Event-B. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 376\u2013393. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33600-8_32"},{"key":"17_CR5","unstructured":"Barlow, R.E., Chatterjee, P.: Introduction to fault tree analysis. Technical report, DTIC Document (1973)"},{"key":"17_CR6","unstructured":"Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability, vol. 185, pp. 825\u2013885 (2009)"},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: Design Automation Conference, pp. 317\u2013320. ACM (1999)","DOI":"10.21236\/ADA360973"},{"key":"17_CR8","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","volume":"58","author":"A Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Adv. Comput. 58, 117\u2013148 (2003)","journal-title":"Adv. Comput."},{"key":"17_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1007\/978-3-662-49674-9_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B Bittner","year":"2016","unstructured":"Bittner, B., et al.: The xSAP safety analysis platform. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 533\u2013539. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_31"},{"key":"17_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"518","DOI":"10.1007\/978-3-319-21690-4_36","volume-title":"Computer Aided Verification","author":"M Bozzano","year":"2015","unstructured":"Bozzano, M., Cimatti, A., Fernandes Pires, A., Jones, D., Kimberly, G., Petri, T., Robinson, R., Tonetta, S.: Formal design and safety analysis of AIR6110 wheel brake system. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 518\u2013535. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_36"},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/978-3-319-08867-9_22","volume-title":"Computer Aided Verification","author":"R Cavada","year":"2014","unstructured":"Cavada, R., et al.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334\u2013342. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_22"},{"key":"17_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/978-3-319-33600-8_33","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"T Fayolle","year":"2016","unstructured":"Fayolle, T., Frappier, M., Gervais, F., Laleau, R.: Modelling a hemodialysis machine using algebraic state-transition diagrams and B-like methods. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 394\u2013408. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33600-8_33"},{"key":"17_CR13","unstructured":"Fresenius Medical Care: 2008T Hemodialysis Machine, User Manual (2008)"},{"key":"17_CR14","unstructured":"Habermaier, A.: Design time and run time formal safety analysis using executable models. Ph.D. thesis, University of Augsburg (2016)"},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"Hasan, O., Tahar, S.: Formal verification methods. In: Encyclopedia of Information Science and Technology, 3rd edn., pp. 7162\u20137170. IGI Global (2015)","DOI":"10.4018\/978-1-4666-5888-2.ch705"},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1007\/978-3-319-33600-8_31","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"TS Hoang","year":"2016","unstructured":"Hoang, T.S., Snook, C., Ladenberger, L., Butler, M.: Validating the requirements and design of a hemodialysis machine using iUML-B, BMotion Studio, and co-simulation. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 360\u2013375. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33600-8_31"},{"key":"17_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-642-40793-2_21","volume-title":"Computer Safety, Reliability, and Security","author":"P Masci","year":"2013","unstructured":"Masci, P., Ayoub, A., Curzon, P., Lee, I., Sokolsky, O., Thimbleby, H.: Model-based development of the generic PCA infusion pump user interface prototype in PVS. In: Bitsch, F., Guiochet, J., Ka\u00e2niche, M. (eds.) SAFECOMP 2013. LNCS, vol. 8153, pp. 228\u2013240. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40793-2_21"},{"issue":"3","key":"17_CR18","doi-asserted-by":"crossref","first-page":"571","DOI":"10.1007\/s11219-015-9288-0","volume":"24","author":"A Mashkoor","year":"2016","unstructured":"Mashkoor, A.: Model-driven development of high-assurance active medical devices. Softw. Qual. J. 24(3), 571\u2013596 (2016)","journal-title":"Softw. Qual. J."},{"key":"17_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/978-3-319-33600-8_29","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"A 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, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33600-8_29"},{"key":"17_CR20","unstructured":"Mashkoor, A., Sametinger, J.: Rigorous modeling and analysis of interoperable medical devices. In: Modeling and Simulation in Medicine Symposium. p. 5. Society for Computer Simulation International (2016)"},{"key":"17_CR21","volume-title":"Failure Mode and Effect Analysis FMEA from Theory to Execution","author":"DH Stamatis","year":"2003","unstructured":"Stamatis, D.H.: Failure Mode and Effect Analysis FMEA from Theory to Execution. ASQ Quality Press, Milwaukee (2003)"},{"issue":"11","key":"17_CR22","first-page":"1006","volume":"171","author":"DM Zuckerman","year":"2011","unstructured":"Zuckerman, D.M., Brown, P., Nissen, S.E.: Medical device recalls and the FDA approval process. Arch. Intern. Med. 171(11), 1006\u20131011 (2011)","journal-title":"Arch. Intern. Med."}],"container-title":["Lecture Notes in Computer Science","SOFSEM 2018: Theory and Practice of Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-73117-9_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,8]],"date-time":"2019-10-08T11:45:02Z","timestamp":1570535102000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-73117-9_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,22]]},"ISBN":["9783319731162","9783319731179"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-73117-9_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017,12,22]]}}}