Formal verification and safety assessment of a hemodialysis machine

• Shaid Khan
• Osman Hasan
• Atif Mashkoor

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.