Many states/transitions formalisms have been proposed in the literature to perform Safety Analyses. In this paper we compare two of them: SAML and AltaRica. These formalisms have been developed by different communities. Their “look-and-feel” are thus quite different. Yet, their underlying mathematical foundations are very similar: both of them rely on state automata. It is therefore of interest to study their ability to assess the reliability of systems, their respective advantages and drawbacks and to seek for opportunities of a cross fertilization.

Debugging a software system is a difficult and time consuming task. This is in particular true for control software in technical systems. Such software typically has a very long life cycle, has been programmed by engineers and not computer scientists, and has been extended numerous times to adapt to a changing environment and new technical products. As a consequence, the software is often not in an ideal condition. Additionally, such software often faces real-time requirements, which often makes it impossible to use dynamic techniques (e. g., single-stepping or tracing). Technically, such software is often realized in C/C++ in a rather imperative programming style. Adaptation and extension is often done by adding configuration parameters. As a consequence, checking for correctness as well as debugging requires to consider the source code as well as its configuration parameters. In this paper, we propose a pragmatic approach to debugging such software. The approach was designed such that (a) it does not require any understanding of the software before starting, and (b) that it can be easily used by programmers and not only by experts. We evaluated the approach on an artificial but realistic case study provided by Robert Bosch GmbH.

The development of safety critical systems often requires design decisions which influence not only dependability, but also other properties which are often even antagonistic to dependability, e.g., cost. Finding good compromises considering different goals while at the same time guaranteeing sufficiently high safety of a system is a very difficult task.We propose an integrated approach for modeling, analysis and optimization of safety critical systems. It is fully automated with an implementation based on the Eclipse platform. The approach is tool-independent, different analysis tools can be used and there exists an API for the integration of different optimization and estimation algorithms. For safety critical systems, a very important criterion is the hazard occurrence probability, whose computation can be quite costly. Therefore we also provide means to speed up optimization by devising different combinations of stochastic estimators and illustrate how they can be integrated into the approach.We illustrate the approach on relevant case-studies and provide experimental details to validate its effectiveness and applicability. (C) 2013 Elsevier Inc. All rights reserved.

The increasing complexity of modern software-intensive systems makes their analysis much more difficult. At the same time, more and more of these systems are used in safety-critical environment. Model based safety analysis can help with this problem by giving provably correct and complete results, very often in a fully automatic way. Today, such methods can cope with logical as well as probabilistic questions. However, very often the models used in many model based approaches must be specified in different input languages depending on the chosen verification tool for the desired aspect, which is time consuming and often error-prone. In this paper, we report on our experiences in designing a tool independent specification language (SAML) for model based safety analysis. This allows to use only one model and analyze it with different methods and different verification engines, while guaranteeing the equivalence of the analyzed models. In particular, we discuss challenges and possible solutions to integrate SAML in the development process of real systems.

Even in the domain of safety critical systems, safety and reliability are not the only goals and a developing engineer is faced with the problem to find good compromises wrt. other antagonistic objectives, in particular economic aspects of a system. Thus there does not exist a single optimal design variant of a system but only compromises each "best" in its own rights. With the rising complexity, especially of cyber-physical systems, the process of manually finding best compromises becomes even more difficult. To cope with this problem, we propose a model-based optimization approach which uses quantitative model-based safety analysis. While the general approach is tool-independent, we implement it technically by introducing well defined variation points to a formal system model. These allow enough variability to cover whole families of systems while still being rigorous enough for formal analysis. From the specification of this family of system variants and a set of objective functions, we compute Pareto optimal sets, which represent best compromises. In this paper we present a framework which allows for optimization of arbitrary quantitative goal functions, in particular probabilistic temporal logic properties used for model-based safety analysis. Nevertheless, the approach itself is well applicable to other domains.

Software-intensive systems become more and more important in safety critical applications, mainly because of the rising number and complexity of embedded system. Many traditional safety analysis techniques where developed decades ago and thus cannot cope with the complexity of modern systems. Model based analysis techniques where developed to deal with the complexity of software-intensive systems. However, due to the lack of tool support these techniques are currently limited to highly skilled experts. Thus model-based analysis is rarely used by system engineers. Based on the safety analysis modeling language (SAML) framework we propose the S 3 E, which integrates a complete safety analysis environment into the eclipse platform. S 3 E covers the whole safety analysis work flow. This implies a powerful editor for model creation, a seamless integration of model-analysis tools and presentation as well as evaluation of the analysis results into one environment. In this paper we present the current state of S 3 E and first experiences with the eclipse plug-in development.

Software controls in technical systems are becoming more and more important and complex. Model based safety analysis can give provably correct and complete results, often in a fully automatic way. These methods can answer both logical and probabilistic questions. In common practice, the needed models must be specified in different input languages of different tools depending on the chosen verification tool for the desired aspect. This is time consuming and error-prone. To cope with this problem we developed the safety analysis modeling language (SAML). In this paper, we present a new tool to intuitively create probabilistic, non-deterministic and deterministic specifications for formal analysis. The goal is to give tool-support during modeling and thus make building a formal model less error-prone. The model is then automatically transformed into the input language of state of the art verification engines. We illustrate the approach on a case-study from nuclear power plant domain.

Software is taking over more and more functionality in most technical systems, which leads to the term software-intensive or cyber-physical systems. Although this offers many exciting new opportunities, it also makes precise analysis of safety and reliability goals much more complicated. Well-known traditional techniques often reach their limits. Model-based approaches on the other hand can be useful for solving some of these problems. However, in industrial practice answering the question alone is often not sufficient. It is also necessary to explain how answers were found. In this paper, we will show some of the capabilities of modern model-based analysis methods and highlight how they possibly could be used in safety engineering resp. what obstacles need to be avoided.