This paper presents a method to include safety system conflicts into a fault tree analysis (FTA) with semantic extensions of fault events. The verification of the incoherent fault tree is done with an SMT-Solver. As an example a networked setup of medical devices for extracorporeal lung assist was analyzed. The method is developed as a basis for improved safety analysis of networked systems.
2.1
Single fault protection for an FTA is given, if every possible chain of faults, caused by a single basic event, additionally requires the malfunction of a safety system to result in a valid top event. Safety related dependencies are used to describe the interaction of safety measures. Focus of our interest are competing measures, which prevent the correct operation. Our example are the goals in a networked system for extracorporeal lung assist, Copyright c by the paper’s authors. Copying permitted for private and academic purposes.
where the blood is oxygenated outside of the body. Safety systems can include the detection of a leak or supervision of a sufficient oxygenation. These can conflict due to their measures which influence the same control value limitation of the blood flow to minimize the loss of blood or ensure sufficient lung assist. A simplified example is given in Fig. 1, with the types of events and existing dependencies discussed below. We adopt the syntax of the Faulttree Handbook [?]. The semantic was extended to allow the modeling of dependencies of two or more safety measures. Three types of events are used, one independent, at least one dependent and exactly one covered event for each dependent event. The formal description of a safety measure dependency is S = (i, D, C) where i is the independent event, D the nonempty set of dependent events and C the nonempty set of covered events.
Independent Events An independent event represents the fault of a safety system. Its correct operation interrupts another conflicting safety measure. An independent event as safety measure is modeled by an intermediate event. In our case it could be the failing safety measure for a leak in the cardiopulmonary bypass.
Dependent Events The dependent event is a basic event which results in the fault of a safety measure and is caused by the successful operation of another safety measure represented by the corresponding independent event. If the independent event is false, all related dependent events are true. The dependent event can be seen as negation of the independent event which results in a non-coherent fault-tree [?].
Covered Event If the fault tree is analyzed for violation of the single fault safety, a dependency generates duplicates of fault chains due to equivalent assignments. The single fault condition allows a single basic event without dependency to be true. The state of basic events which are dependent events is the negation of the related independent (safety) event. Valid assignments which create the same fault chain, unrelated to dependent events, differ in the possible states of the dependent events. The events, semantically extended to be covered events, are the events directly associated with a safety event. This coverage can be violated by a dependency of the covering safety event. Any corresponding dependent event as part of the covering safety event is only active, if the covered event is true. In the following we show which dependencies have to be considered. Dependencies which create duplicates of fault chains will be blocked. The dependency between safety measures is now assumed to be bidirectional.
• Φ set of all covered events • Ψ set of all safety events • Ψrel set of all relevant safety events • Ω ⊆ Ψ set of all covering safety events • Θ ⊆ Ψ set of safety events in conflict with a safety event ω ∈ Ω • Φsel ⊆ Φ set of all covered and fulfilled events • θ ∈ Θ a safety event which interrupts a safety event ω ∈ Ω • Ψelim set of all irrelevant safety events For every covered event ϕ ∈ Φsel the corresponding safety event ψ ∈ Ψ is added to Ω. For each ω ∈ Ω all interrupting dependent events are identified. For each of the dependent events independent event ψ ∈ Ψ is added to Θ. The safety events which are further handled as irrelevant, because they interrupt with Θ, are given by Ψelim = Ψ\ (Ω ∪ Θ). Three cases of interactions can be distinguished for dependencies between safety measures: 1. An interaction between irrelevant safety events in Ψelim and has to be blocked. There exists no dependency allowing ψ ∈ Ψ causing a fault for a ψelim ∈ Ψelim and for a ω ∈ Ω. Otherwise ψ would be element of Θ. The dependency of an independent event ψ ∈ Ψelim is irrelevant and blocked, because it does not contain covered events in Φsel. Otherwise Θ would contain its independent event, due to its dependency on ω ∈ Ω which covers a ϕ ∈ Φsel. 2. An interaction between safety events in the set of covered events Θ. Two variable assignments exist, which cause a fault in ψ ∈ Ψ. The dependency between the safety events θ1 ∈ Θ and θ2 ∈ Θ create these two assignments which only differ in the state of θ1 or θ2 (Fig. 1), which can be combined by blocking. 3. An interaction between safety events in Ψrel = Ω ∪ Θ and Ψelim = Ψ\(Ω ∪ Θ). θ ∈ Θ is influenced by the dependency on ψelim ∈ Ψelim , or vice versa. Only the active θ is relevant, because it is able to create a fault in ψ ∈ Ω and could influence the fulfillment of the top event. Because no independent event ψelim ∈ Ψelim exists in Φsel the dependencies causing a fault in θ are blocked.
There exists a dependency for a θ ∈ Θ to a ψ ∈ Ω for every ψ which has a dependency with θ because of the assumption of bidirectional dependencies. On the one hand ψ ∈ Ω can be interrupted which allows the fulfillment of the top event. On the other hand θ can be interrupted and therefore not influence any other event. If ψ ∈ Ω is not fulfilled, all ψ interrupting θ ∈ Θ have to be fulfilled. As a result the top event cannot be fulfilled and the covering safety event becomes irrelevant. 3 3.1
The fault tree is parsed according to [?], with subsumed soundness and completeness. The AND- and OR-gates conditions are ψ ↔ (ϕ1 ∧ ϕ2) and Ψ ↔ (ϕ1 ∨ ϕ2), respectively. The tree is parsed top down by checking the successors of every intermediate events, until an event is found, which is not an intermediate event. The result is a logical equivalence with a successor event or with an logical term for a gate and its successors. 3.2
All relevant information of an event, such as its dependencies, is stored in a global list. Based on this list, an additional list with dependencies is generated. The dependency is relevant, if the covered event is fulfilled. This leads to
K = c1 ∨ c2 . . . cn, n = |C|, C ∈ S as a formal condition for activation of a dependency S, with the covered event ci ∈ C. The value v of a dependent event is given by v = ¬i ∧ K, with independent event i and activation condition K. d ↔ v is generated for every dependent event d ∈ D of a safety measure dependency S. 3.3
For Φ as a set of basic events in a tree we define Φb ⊆ Φ as the subset of all basic events according to the semantics of [?] and Φd ⊂ Φ the set of all dependent basic events caused by a interrupting safety measure with Φb ∪ Φd = ∅. For every pair of b1, . . . bn ∈ Φb, with n = |Φb| is ¬(bi ∧ bj) created, where i, j ∈ {1, . . . , n} and i 6= j. This is only satisfiable if no pair exists where both are valid the same time. An existing open source tool with XML support was used [?]. The modeled fault trees were analyzed for dependencies. As result minimal fault trees were identified. These trees represent the fault chain from a top event, that means the violation of a safety goal, to the responsible basic event. The minimal trees include only these events, that are true for the occurring basic event. Since a fault tree modeled with dependencies is incoherent, the analysis is more complex. This reason and the option to use arithmetic information motivated the use of an SMT2-Solver. The fault tree was processed according to the parsing methods above to generate input in form of Boolean expressions which were checked for satisfiability with the SMT-solver. Because it is supported by several well known solvers the parsed input is in SMT-Lib format. Here SMTInterpol was used [?]. The solver finds a valid variable assignment which fulfills a top event according to the single fault condition. This is done iteratively with exclusion of the models found by including their negation until no assignment can be found by the solver. A description in form of the relevant tree is given by comparing the set of logical equivalents (cf. Sect. 3) with an identified assignment. Further a report about the events which violate the single fault condition and their fault chain is generated, which includes information describing the events. Minimal fault trees which were identified are reported in this form: ”safety goal 4: loss of blood in extracorporeal circuit” ← ... ”leak detection fails” ← ”leak” ∧(¬ ”oxygenation supervision fails”) (Fig. 1). In case of the worked example 7 safety goals were defined. 13 dependencies between safety measures were identified in the existing FTA and therefore 42 dependent events were added to include the conflicts. The valid assignments which violate the single fault condition were increased from 21 to 52. It has to be noted, that the safety dependencies are over-approximated, since detailed behavior is not modeled yet. 5
The problem of undesired equivalent results as described in Sect. 2.2 could be handled by quantifier elimination [?], which is a more general approach, but in case of this problem less efficient. The SAT-Solver has to be used at least once for each time the elimination algorithm is used for an equivalence class. Other examples of safety analysis methods with SMT-Solvers can be found in the work of Bozzano et al. [?], but do not handle conflicts in FTAs and therefore differ in usage of the solver. 6
A method to increase the accuracy of an FTA by modeling dependencies of existing safety measures was presented. It can be used to prove the single fault safety of a system based on the FTA. The fault tree syntax was not changed and the semantic only extended. Detailed reports about violations of the single fault safety were generated with the use of an SMT-Solver. They include the violating fault chain, from responsible basic event to the violated top event. The computation time needed for the example mentioned above on a consumer notebook (i.e. Intel i5-3320M, 4GB DDR2) was always below 20 seconds. The presented method allows to include possible conflicts of networked cyber-medical systems and verification of these fault trees with increased complexity.
Further our method is thought as basis to connect high- and low-level methods to support safety and reliability during the design of networked systems with significant safety demands. Currently the computational efficiency of this method is tested more detailed and estimated for increasing tree size. To improve the FTA the types of supported events can be extended according to [?] to allow the modeling of priorities, which decreases the number of false positives. Over-approximation can be further reduced by including arithmetic information for the SMT-Solver, provided by detailed models.
This work was supported by the German Research Foundation DFG (DFG - Grant PAK 138/2). The authors gratefully acknowledge this allowance.