The following lists contain a selection of peer-reviewed publications written by the Institute for Software & Systems Engineering (ISSE) in the context of model-based safety analysis with S#.

• Leupolz, J.: Probabilistic Safety Analysis of Executable Models. PhD thesis. OPUS Augsburg, 2018 (Evaluation results and proofs)

  Abstract: Classical software verification focuses on answering the question if the implementation of a piece of software conforms to a specification. Verification plays an essential role in safety-critical domains like railway, automotive, aviation, and also medical devices. Another crucial aspect in those domains is the analysis what happens if a specification-conforming system is embedded into a dangerously behaving environment or if parts of the system (e.g., sensors or radio-devices) are malfunctioning. Even under such problematic circumstances, the operation of a safety-critical system should not lead to accidents or cause any other form of harm. Traditional safety techniques like the fault tree analysis describe a way how an upper bound of the hazard probability can be estimated using the probabilities of the component faults, but these traditional safety-analysis techniques have not been designed for software-intensive systems. Because of their complex behavior, such software-intensive systems are hard to analyze. This thesis presents an approach how such systems can be modeled and analyzed probabilistically using executable modeling languages, i.e., modeling languages that model behavior in an executable way; as a consequence, the approach mitigates problems that arise in the probabilistic analysis of software-intensive systems.

• Leupolz, J.,Habermaier, A., Reif, W.: Quantitative and Qualitative Safety Analysis of a Hemodialysis Machine with S#. Journal of Software: Evolution and Process. Wiley, 2018 (Evaluation results)

  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.

• Leupolz, J., Knapp, A., Habermaier, A., Reif, W.: Qualitative and Quantitative Analysis of Safety-Critical Systems with S#. In International Journal on Software Tools for Technology Transfer. Springer, 2017 (Evaluation results, view only)

  Abstract: We give an overview of the S# (pronounced “safety sharp”) framework for rigorous, model-based analysis of safety-critical systems. We introduce S#’s expressive modeling language based on the C# programming language, showing how S#’s fault modeling and flexible model composition capabilities can be used to model a case study from the transportation sector with multiple design variants. A formal semantics for executable probabilistic models is given. Fully automated qualitative and quantitative safety analyses are conducted for the case study using algorithms of the model checkers LTSmin and MRMC. The results of the quantitative analyses are discussed in comparison to results obtained by using traditional techniques.

• Habermaier, A.: Design Time and Run Time Formal Safety Analysis using Executable Models. PhD thesis. OPUS Augsburg, 2017

  Abstract: The contribution of this thesis is a systematic design time and run time modeling and analysis approach for safety-critical systems based on formal methods and executable models. Its main achievements are threefold: Firstly, a systematic modeling approach and the executable modeling language S# are introduced. Secondly, a safety analysis technique based on explicit-state model checking and its formal foundations are defined, increasing analysis efficiency and practical usability compared to alternative techniques. Thirdly, a unified model execution and analysis approach is used to simulate and visualize S# models and to systematically conduct design time and run time safety analyses for them with consistent semantics. The contributions are evaluated using different case studies from multiple application domains.

• Klumpp, D., Habermaier, A., Eberhardinger, B., Seebach, H.: Optimising Runtime Safety Analysis Efficiency for Self-Organising Systems. In Self-Adaptive and Self-Organizing Systems Workshops. IEEE, 2016

  Abstract: Self-organising resource-flow systems typically have a high tolerance for component faults: When a component fails, the system can use another component of the same type instead. However, this redundancy is eventually exhausted: If enough components fail, they can no longer be replaced and the system ceases to function. An analysis of these self-organisation limits is essential to assess the system’s safety but difficult to perform at design time because the system’s structure and behaviour are hard to predict. By contrast, runtime analyses are subject to high performance demands. This paper presents several techniques that significantly reduce analysis time in order to facilitate safety analyses at runtime. We model a self-organising system producing personalised medicine and use it to evaluate these techniques.

• Habermaier, A., Leupolz, J., Reif, W.: Unified Simulation, Visualization, and Formal Analysis of Safety-Critical Systems with S#. In FMICS-AVoCS 2016. Springer, 2016

  Abstract: We give an overview of the S# (pronounced "safety sharp") framework for rigorous, model-based analysis of safety-critical systems. We introduce S#’s expressive modeling language based on the C# programming language, showing how S#’s fault modeling and flexible model composition capabilities can be used to model a case study from the transportation sector with multiple design variants. Fully automated formal safety analyses are conducted for the case study using the explicit-state model checker LTSmin. Analysis efficiency is evaluated in comparison with other safety analysis tools and model checkers.

• Habermaier, A., Knapp, A., Leupolz, J., Reif, W.: Fault-Aware Modeling and Specification for Efficient Formal Safety Analysis. In FMICS-AVoCS 2016. Springer, 2016

  Abstract: Deductive Cause Consequence Analysis (DCCA ) is a model checking- based safety analysis technique that determines all combinations of faults potentially causing a hazard. This paper introduces a new fault modeling and specification approach for safety-critical systems based on the concept of fault activations that decreases explicit-state model checking and safety analysis times by up to three orders of magnitude. We augment Kripke structures and LTL with fault activations and show how standard model checkers can be used for analysis. Additionally, we present conceptual changes to DCCA that improve efficiency and usability. We evaluate our work using our safety analysis tool S# ("safety sharp").

• Leupolz, J., Habermaier, A., Reif, W.: Safety Analysis of a Hemodialysis Machine with S#. In EuroAsiaSPI 2016 Industrial Proceedings. Whitebox, 2016. slides

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

• Eberhardinger, B., Habermaier, A., Seebach, H., Reif, W.: Back-to-Back Testing of Self-Organization Mechanisms. In ICTSS 2016. Springer, 2016

  Abstract: When developing SO mechanisms, mapping requirements to actual designs and implementations demands a lot of expertise. Among other things, it is important to define the right degree of freedom for the system that allows for self-organization. Back-to-back testing supports this hard engineering task by an adequate testing method helping to reveal failures in this design and implementation procedure. Within this paper we propose a model-based approach for back-to-back testing. The approach is built on top of the S# framework and integrated into the Visual Studio development environment, enabling the creation of executable test models with comprehensive tooling support for model debugging. By applying the concepts to a self-organizing production cell, we show how it is used to fully automatically reveal faults of a SO mechanism.

• Eberhardinger B., Habermaier, A., Hoffmann, A., Poeppel, A., Reif, W.: Toward Integrated Analysis & Testing of Component-Based, Adaptive Robot Systems. In Verification and Validation of Adaptive Software Systems. IEEE, 2016

• Habermaier, A., Eberhardinger, B., Seebach, H., Leupolz, J., Reif, W.: Runtime Model-Based Safety Analysis of Self-Organizing Systems with S#. In: Self-Adaptive and Self-Organizing Systems Workshops, 2015

  Abstract: Self-organizing systems present a challenge for model-based safety analysis techniques: At design time, the potential system configurations are unknown, making it necessary to postpone the safety analyses to runtime. At runtime, however, model checking based safety analysis techniques are often too time-consuming because of the large state spaces that have to be analyzed. Based on the S# framework's support for runtime model adaptation, we modularize runtime safety analyses by splitting them into two parts, modeling and analyzing the self-organizing and non-self-organizing parts separately. With some additional heuristics, the resulting state space reduction facilitates the use of model checking based safety analysis techniques to analyze the safety of self-organizing systems. We outline this approach on a self-organizing production cell, assessing the self-organization's impact on the overall safety of the system.

• Habermaier, A., Leupolz, J., Reif, W.: Executable Specifications of Safety-Critical Systems with S#. In: Dependable Control of Discrete Systems, pp. 60–65. IFAC, 2015

  Abstract: Model-based safety analysis techniques use formal methods to rigorously assess the risks associated with safety-critical systems. The adequacy of the results obtained from those formal techniques, however, is greatly influenced by the quality and comprehensibility of the underlying formal models. We introduce our S# modeling framework (pronounced "safety sharp"), an executable, systematic, high-level specification language and tool suite specifically designed for the convenient modeling and formal analysis of safety-critical systems. This paper shows how S# facilitates and improves model simulation, debugging, and testing during all stages of the development of such systems.