Premium
Quantitative and qualitative safety analysis of a hemodialysis machine with S#
Author(s) -
Leupolz Johannes,
Habermaier Axel,
Reif Wolfgang
Publication year - 2018
Publication title -
journal of software: evolution and process
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.371
H-Index - 29
eISSN - 2047-7481
pISSN - 2047-7473
DOI - 10.1002/smr.1942
Subject(s) - toolchain , hazard analysis , hazard , computer science , component (thermodynamics) , static analysis , software , system safety , model checking , reliability engineering , software engineering , risk analysis (engineering) , programming language , engineering , medicine , chemistry , physics , organic chemistry , thermodynamics
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.