Formal verification and safety assessment of a hemodialysis machine

Autoren Shaid Khan
Osman Hasan
Atif Mashkoor
Editoren A Min Tjoa
Ladjel Bellatreche
Stefan Biffl
Jan van Leeuwen
Jiří Wiedermann
Titel Formal verification and safety assessment of a hemodialysis machine
Buchtitel SOFSEM 2018: Theory and Practice of Computer Science - Proc. SOFSEM 2018
Typ in Konferenzband
Verlag Edizioni della Normale
Serie Lecture Notes in Computer Science
Band 10706
ISBN 978-3-319-73116-2
DOI 10.1007/978-3-319-73117-9_17
Monat January
Jahr 2018
Seiten 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.