Safety Analysis of a Hemodialysis Machine with S#

This paper reports 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 (DCCA), a fully automatic model checking-based safety analysis technique that de-termines all sets of component faults with the potential of causing a system hazard. 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 DCCA.
EuroAsiaSPI 2016 Industrial Proceedings

Publisher: Whitebox, Denmark

ISBN: 978-87-998116-6-3


For questions regarding the publication, please contact!