Formal verification and safety assessment of a hemodialysis machine

Authors Shaid Khan
Osman Hasan
Atif Mashkoor
Editors A Min Tjoa
Ladjel Bellatreche
Stefan Biffl
Jan van Leeuwen
Jiří Wiedermann
Title Formal verification and safety assessment of a hemodialysis machine
Booktitle SOFSEM 2018: Theory and Practice of Computer Science - Proc. SOFSEM 2018
Type in proceedings
Publisher Edizioni della Normale
Series Lecture Notes in Computer Science
Volume 10706
ISBN 978-3-319-73116-2
DOI 10.1007/978-3-319-73117-9_17
Month January
Year 2018
Pages 241-254
SCCH ID# 17061

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. Classical approaches used for safety assessment includes Fault Tree Analysis (FTA) and Failure Mode and Effect Analysis (FMEA). Traditionally, safety assessment of a system is done analytically or using simulation based tools. How- ever, 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 (xSAP) is used to check various undesired behaviors of the system using invariant properties defined as Top Level Events (TLE). This way, we can automatically generate the FTA and FMEA to do the safety assessment of the given Hemodialysis machine.