A Survey of Safety Analysis Techniques for Safety Critical Systems
---
paper_title: Software safety: why, what, and how

paper_content:

Software safety issues become important when computers are used to control real-time, safety-critical processes. This survey attempts to explain why there is a problem, what the problem is, and what is known about how to solve it. Since this is a relatively new software research area, emphasis is placed on delineating the outstanding issues and research topics.
---
paper_title: Validating Safety Models with Fault Trees

paper_content:

In verifying a safety-critical system, one usually begins by building a model of the basic system and of its safety mechanisms. If the basic system model does not reflect reality, the verification results are misleading. We show how a model of a system can be compared with the system’s fault trees to help validate the failure behaviour of the model. To do this, the meaning of fault trees are formalised in temporal logic and a consistency relation between models and fault trees is defined. An important practical feature of the technique is that it allows models and fault trees to be compared even if some events in the fault tree are not found in the system model.
---
paper_title: DEDUCTIVE CAUSE-CONSEQUENCE ANALYSIS (DCCA)

paper_content:

Abstract In this paper we present a new form of formal safety analysis: deductive cause-consequence analysis (DCCA). Deductive Cause-Consequence Analysis is a way to use formal methods for safety analysis. It substitutes error-prone informal reasoning by mathematical proofs. DCCA allows to rigorously prove whether a failure on component level is the cause for system failure or not. DCCA is a formal generalization of the two most common safety analysis techniques: failure modes and effects analysis (FMEA) and fault tree analysis (FTA). We apply the method to a real world case study: the height control in the Elbe-tunnel in Hamburg. This shows how formal safety analysis with DCCA helps identifying design flaws and weaknesses in a real-world industrial system.
---
paper_title: A comparison of two approaches to safety analysis based on use cases

paper_content:

Engineering has a long tradition in analyzing the safety of mechanical, electrical and electronic systems. Important methods like HazOp and FMEA have also been adopted by the software engineering community. The misuse case method, on the other hand, has been developed by the software community as an alternative to FMEA and preliminary HazOp for software development. To compare the two methods misuse case and FMEA we have run a small experiment involving 42 third year software engineering students. In the experiment, the students should identify and analyze failure modes from one of the use cases for a commercial electronic patient journals system. The results of the experiment show that on the average, the group that used misuse cases identified and analyzed more user related failure modes than the persons using FMEA. In addition, the persons who used the misuse cases scored better on perceived ease of use and intention to use.
---
paper_title: Safety Analysis Using Petri Nets

paper_content:

The application of Time Petri net modeling and analysis techniques to safety-critical real-time systems is explored and procedures described which allow analysis of safety, recoverability, and fault-tolerance.
---
paper_title: Automated multiple failure FMEA

paper_content:

Abstract Failure mode and effects analysis (FMEA) is typically performed by a team of engineers working together. In general, they will only consider single point failures in a system. Consideration of all possible combinations of failures is impractical for all but the simplest example systems. Even if the task of producing the FMEA report for the full multiple failure scenario were automated, it would still be impractical for the engineers to read, understand and act on all of the results. This paper shows how approximate failure rates for components can be used to select the most likely combinations of failures for automated investigation using simulation. The important information can be automatically identified from the resulting report, making it practical for engineers to study and act on the results. The strategy described in the paper has been applied to a range of electrical subsystems, and the results have confirmed that the strategy described here works well for realistically complex systems.
---
paper_title: Modalities for model checking: branching time logic strikes back

paper_content:

Abstract We consider automatic verification of finite state concurrent programs. The global state graph of such a program can be viewed as a finite (Kripke) structure, and a model checking algorithm can be given for determining if a given structure is a model of a specification expressed in a propositional temporal logic. In this paper, we present a unified approach for efficient model checking under a broad class of generalized fairness constraints in a branching time framework extending that of Clarke et al. (1983). Our method applies to any type of fairness expressed in a certain canonical form. Almost all ‘practical’ types of fairness from the literature, including the fundamental notions of impartiality, weak fairness, and strong fairness, can be succintly written in our canonical form. Moreover, our branching time approach can easily be adapted to handle types of fairness (such as fair reachability of a predicate) which cannot even be expressed in a linear temporal logic. We go on to argue that branching time logic is always better than linear time logic for model checking. We show that given any model checking algorithm for any system of linear time logic (in particular, for the usual system of linear time logic) there is a model checking algorithm of the same order of complexity (in both the structure and formula size) for the corresponding full branching time logic which trivially subsumes the linear time logic in expressive power (in particular, for the system of full branching time logic CTL * ). We also consider an application of our work to the theory of finite automata on infinite strings.
---
paper_title: Validating Safety Models with Fault Trees

paper_content:

In verifying a safety-critical system, one usually begins by building a model of the basic system and of its safety mechanisms. If the basic system model does not reflect reality, the verification results are misleading. We show how a model of a system can be compared with the system’s fault trees to help validate the failure behaviour of the model. To do this, the meaning of fault trees are formalised in temporal logic and a consistency relation between models and fault trees is defined. An important practical feature of the technique is that it allows models and fault trees to be compared even if some events in the fault tree are not found in the system model.
---
paper_title: Formal fault tree semantics

paper_content:

In train control systems, more and more (electro-)mechanical devices are substituted by software based devices. To sustain the high level safety standards for these embedded systems, we propose the integration of fault tree analysis and formal methods. This combines two important safety analysis methods from the involved domains of engineering and software development. Our approach proposes to build a formal model of the system together with fault trees, which investigate the safety critical aspects by breaking them down to software and hardware requirements. The events of fault trees are formalized with respect to the model. Formal completeness and correctness conditions are given, using Interval Tempo- ral Logic with continuous semantics. They define a formal semantics of fault trees, which allows cause-consequence relations between events in addition to boolean decomposi- tion. The semantics is therefore suitable for dynamic sys- tems. We will prove, that the conditions guarantee, that the fault tree is a correct and complete analysis of the causes of the considered fault.
---
paper_title: Combining Formal Methods and Safety Analysis - The ForMoSA Approach

paper_content:

In the ForMoSA project [18] an integrated approach for safety analysis of critical, embedded systems has been developed. The approach brings together the best of engineering practice, formal methods and mathematics: traditional safety analysis, temporal logics and verification, and statistics and optimization.
---
paper_title: Modalities for model checking: branching time logic strikes back

paper_content:

Abstract We consider automatic verification of finite state concurrent programs. The global state graph of such a program can be viewed as a finite (Kripke) structure, and a model checking algorithm can be given for determining if a given structure is a model of a specification expressed in a propositional temporal logic. In this paper, we present a unified approach for efficient model checking under a broad class of generalized fairness constraints in a branching time framework extending that of Clarke et al. (1983). Our method applies to any type of fairness expressed in a certain canonical form. Almost all ‘practical’ types of fairness from the literature, including the fundamental notions of impartiality, weak fairness, and strong fairness, can be succintly written in our canonical form. Moreover, our branching time approach can easily be adapted to handle types of fairness (such as fair reachability of a predicate) which cannot even be expressed in a linear temporal logic. We go on to argue that branching time logic is always better than linear time logic for model checking. We show that given any model checking algorithm for any system of linear time logic (in particular, for the usual system of linear time logic) there is a model checking algorithm of the same order of complexity (in both the structure and formula size) for the corresponding full branching time logic which trivially subsumes the linear time logic in expressive power (in particular, for the system of full branching time logic CTL * ). We also consider an application of our work to the theory of finite automata on infinite strings.
---
paper_title: DEDUCTIVE CAUSE-CONSEQUENCE ANALYSIS (DCCA)

paper_content:

Abstract In this paper we present a new form of formal safety analysis: deductive cause-consequence analysis (DCCA). Deductive Cause-Consequence Analysis is a way to use formal methods for safety analysis. It substitutes error-prone informal reasoning by mathematical proofs. DCCA allows to rigorously prove whether a failure on component level is the cause for system failure or not. DCCA is a formal generalization of the two most common safety analysis techniques: failure modes and effects analysis (FMEA) and fault tree analysis (FTA). We apply the method to a real world case study: the height control in the Elbe-tunnel in Hamburg. This shows how formal safety analysis with DCCA helps identifying design flaws and weaknesses in a real-world industrial system.
---
paper_title: A comparison of two approaches to safety analysis based on use cases

paper_content:

Engineering has a long tradition in analyzing the safety of mechanical, electrical and electronic systems. Important methods like HazOp and FMEA have also been adopted by the software engineering community. The misuse case method, on the other hand, has been developed by the software community as an alternative to FMEA and preliminary HazOp for software development. To compare the two methods misuse case and FMEA we have run a small experiment involving 42 third year software engineering students. In the experiment, the students should identify and analyze failure modes from one of the use cases for a commercial electronic patient journals system. The results of the experiment show that on the average, the group that used misuse cases identified and analyzed more user related failure modes than the persons using FMEA. In addition, the persons who used the misuse cases scored better on perceived ease of use and intention to use.
---

Title: A Survey of Safety Analysis Techniques for Safety Critical Systems

Section 1: INTRODUCTION
Description 1: Introduce the importance and definition of safety critical systems, and provide an overview of the paper's focus on both formal and informal safety analysis techniques.

Section 2: ANALYSIS OF SAFETY APPROACHES
Description 2: Analyze different safety analysis approaches, divided into informal (traditional) techniques and formal techniques.

Section 3: Informal (Traditional Techniques)
Description 3: Discuss various traditional safety analysis methods such as FMEA, FTA, FHA, and Petri nets, highlighting their strengths and weaknesses.

Section 4: Formal Techniques
Description 4: Examine rigorous formal techniques such as DCCA, FFTA, FSSA, and the integration of UML, focusing on their methodologies, benefits, and limitations.

Section 5: CONCLUSION
Description 5: Summarize the findings of the survey, emphasizing the advantages of combining formal and informal techniques and outlining the direction for future research.