Quantitative and Qualitative Safety Analysis of a Hemodialysis Machine with S#

This paper reports on our experiences of applying S# ("safety sharp") to model and analyze the case study "hemodialysis machine." The S# safety analysis approach focuses on the question, what happens if we place a controller with correct software into an unreliable environment. To answer that question, the S# toolchain natively supports the Deductive Cause Consequence Analysis, a fully automatic model checking‐based safety analysis technique that determines all sets of component faults with the potential of causing a system hazard. Furthermore, S# can give an approximate estimate of the hazard's probability. To demonstrate our approach, we created a model with a simplified controller of the hemodialysis machine and relevant parts of its environment and performed a safety analysis using Deductive Cause Consequence Analysis.
Journal of Software: Evolution and Process

Publisher: Wiley

DOI: 10.1002/smr.1942


For questions regarding the publication, please contact!