Quantitative and qualitative safety analysis of a hemodialysis machine with S#. Issue 5 (21st February 2018)

• Record Type: Journal Article
• Authors: Leupolz, Johannes; Habermaier, Axel; Reif, Wolfgang
• Other Names: Mashkoor Atif guestEditor.; Biró Miklós guestEditor.; Messnarz Richard guestEditor.; Colomo‐Palacios Ricardo guestEditor.
• Is Part Of: Journal of software. Volume 30:Issue 5(2018)
• Page Start: n/a
• Page End: n/a
• Publication Date: 2018-02-21
• Subjects: deductive cause consequence analysis -- design tools and techniques -- embedded domain specific language -- executable models -- formal methods -- hemodialysis -- model checking -- quantitative analysis -- safety analysis -- simulation; Software engineering -- Periodicals; Computer software -- Development -- Periodicals; Software maintenance -- Periodicals; 005.1
• DOI: 10.1002/smr.1942
• Languages: English
• ISSNs: 2047-7473

Abstract

Abstract: 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.