Abstract
Given the safety-critical nature of healthcare systems, their rigorous safety assessment, in terms of studying their behavior in the presence of potential faults and how the malfunctioning components cause system failures, is of paramount importance. Traditionally, the safety assessment of a system is done analytically or using simulation based tools. However, the former is prone to human error and the later does not provide a complete analysis, which makes them inappropriate for the safety assessment of healthcare systems. These limitations can be overcome by using formal methods based safety assessment. This paper presents our experience of applying model based safety assessment and system verification tools on a hemodialysis machine. In particular, we use the nuXmv model checker to formally verify a formal model of the given hemodialysis machine. The formal model of the given system is then extended with various fault modes of the system components and the eXtended Safety Assessment Platform is used to check various undesired behaviors of the system using invariant properties defined as Top Level Events. This way, we can automatically generate the FTA and FMEA to do the safety assessment of the given hemodialysis machine.
The research presented in this paper is partially supported by the Austrian Ministry for Transport, Innovation and Technology, the Federal Ministry of Science, Research and Economy, and the Province of Upper Austria in the frame of the COMET center SCCH.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
ReliaSoft: http://www.reliasoft.com/.
- 2.
Courtesy: Fresenius Medical Care: url: http://fmcna.com//).
- 3.
The codes and associated properties are available at: http://save.seecs.nust.edu.pk/projects/fvsahm/.
References
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–54. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-20615-8_3
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)
Baier, C., Katoen, J.P., Larsen, K.G.: Principles of Model Checking. MIT Press, Cambridge (2008)
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–393. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-33600-8_32
Barlow, R.E., Chatterjee, P.: Introduction to fault tree analysis. Technical report, DTIC Document (1973)
Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability, vol. 185, pp. 825–885 (2009)
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–320. ACM (1999)
Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Adv. Comput. 58, 117–148 (2003)
Bittner, B., et al.: The xSAP safety analysis platform. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 533–539. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49674-9_31
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ăsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 518–535. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_36
Cavada, R., et al.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334–342. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_22
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–408. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-33600-8_33
Fresenius Medical Care: 2008T Hemodialysis Machine, User Manual (2008)
Habermaier, A.: Design time and run time formal safety analysis using executable models. Ph.D. thesis, University of Augsburg (2016)
Hasan, O., Tahar, S.: Formal verification methods. In: Encyclopedia of Information Science and Technology, 3rd edn., pp. 7162–7170. IGI Global (2015)
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–375. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-33600-8_31
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âniche, M. (eds.) SAFECOMP 2013. LNCS, vol. 8153, pp. 228–240. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40793-2_21
Mashkoor, A.: Model-driven development of high-assurance active medical devices. Softw. Qual. J. 24(3), 571–596 (2016)
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–343. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-33600-8_29
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)
Stamatis, D.H.: Failure Mode and Effect Analysis FMEA from Theory to Execution. ASQ Quality Press, Milwaukee (2003)
Zuckerman, D.M., Brown, P., Nissen, S.E.: Medical device recalls and the FDA approval process. Arch. Intern. Med. 171(11), 1006–1011 (2011)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG
About this paper
Cite this paper
Khan, S., Hasan, O., Mashkoor, A. (2018). Formal Verification and Safety Assessment of a Hemodialysis Machine. In: Tjoa, A., Bellatreche, L., Biffl, S., van Leeuwen, J., Wiedermann, J. (eds) SOFSEM 2018: Theory and Practice of Computer Science. SOFSEM 2018. Lecture Notes in Computer Science(), vol 10706. Edizioni della Normale, Cham. https://doi.org/10.1007/978-3-319-73117-9_17
Download citation
DOI: https://doi.org/10.1007/978-3-319-73117-9_17
Published:
Publisher Name: Edizioni della Normale, Cham
Print ISBN: 978-3-319-73116-2
Online ISBN: 978-3-319-73117-9
eBook Packages: Computer ScienceComputer Science (R0)