Based on the above discussion and analysis, we present our formal fault tree construction model below.
We take a catastrophic failure as the root node of the fault tree, namely R. Assume R is a conjunct fault event consisting of two normal events, i.e., oi = p∧oj = qα, the regression procedure for the formal fault tree construction is as follows (in caseR is not a conjunct fault event that consists of only one fault eventoi =p, the regression procedure is straightforward and can be regarded as a simple instantiation of the following procedure).
Initial step Define the formal specification of R≡oi =p∧oj =qα. Regression step
Let A1 ∨. . .∨An ⇒ oi = p be the transition rule selected, and Ah (h = 1, . . . , n) complies with the constraint, that is, Ah 6=> oj = qβ, where qβ denotes any other observation value ofoj except qα.
• For each Ah, if Ah does not contain oj = qα or any oj = qβ, then Mh :=
Ah∧oj =qα, else Mh :=Ah, where Mh is a intermediate variable.
• R :=M1 ∨M2 ∨. . .∨Mn
Iteration step
(1) Decompose the resulting R to some sub-events by an appropriate logic gate or edge;
(2) Integrate and record the corresponding transition rule into the logic gate or edge for further revision;
(3) Then for each sub event, redo the inductive and iteration steps recursively until a basic event or the chosen abstraction level is reached.
To better understand the above formal fault tree construction model and procedure, we can use the crossing control example from Section 3.1.1 as an illustration. In the crossing control system, the root node of collision is formally defined as:
R : pos(T1) =crossing∧bar =open
Then we focus on the event “pos(T1) = crossing” to analyze which conditions will cause a collision to occur. We get the following transition rule:
τ1 : pos(T1) = sect1∧signal-bypass(T1)
∨ pos(T1) = sect1∧err-brake(T1)
∨ pos(T1) = sect1∧level(T1) =state2∧ ¬err-comm(T1)
=> pos(T1) = crossing
This transition rule complies with the constraint, i.e., neither of Ah will change the value ofbar, and We thereby formally derive the following formula:
pos(T1) =sect1∧signal-bypass(T1)∧bar =open∨ pos(T1) =sect1∧err-brake(T1)∧bar =open∨
pos(T1) =sect1∧level(T1) =state2∧ ¬err-comm(T1)∧bar =open
According to the structure of this formula, we thereby obtain three sub-events by adding an T-OR-gate with the root node R.
S1a : pos(T1) =sect1∧signal-bypass(T1)∧bar =open S1b : pos(T1) = sect1∧err-brake(S, T1)∧bar =open
S1c : pos(T1) = sect1∧level(T1) =state2∧ ¬err-comm(T1)∧bar =open
Here, we regard signal-bypass(T1) and err-brake(T1) as basic fault events, and since either pos(T1) = sect1 or bar = open is a normal event, and their conjunction does not constitute a conjunct fault event, an INHIBIT-gate with the CONDITIONING-event pos(T1) =sect1∧bar =opencan be introduced to further simplify S1a and S1b as shown in Figure 5.2. Two basic events B1 and B2 with a CONDITIONING-event C1 is defined as follows.
B1 : signal-bypass(T1) B2 : err-brake(T1)
C1 : pos(T1) =sect1∧bar =open
It should be figured out that, the function range of an CONDITIONING-event is limited to the specific logic gate that it connects to. In other words, an event which is regarded as a CONDITIONING-event for a specific logic gate does not mean that, this event can also be identified as a global CONDITIONING-event in the fault trees.
Then we focus on S1c, it can also be simplified by an INHIBIT-gate, and we get a simplified conjunct fault event S1cs and a CONDITIONING-event C2 as follows.
S1cs : level(T1) = state2∧bar =open C2 : pos(T1) =sect1∧ ¬err-comm(T1)
We regardC2as a CONDITIONING-event becauseS1cscan be identified as a conjunct fault event (the level crossing has sent a ‘release’ permission to a train, but the barriers are still open), and both pos(T1) = sect1 (a train is waiting for the ‘release’ permission to pass the crossing) and ¬err-comm(T1) (no radio communication error occurs) as well as their conjunction are normal events.
Focused on the event level(T1) = state2 of S1cs, one transition rule to cause the level crossing to send a ‘release’ signal to a train is that, the level crossing has accepted and confirmed a ‘secure’ signal from the train, i.e., level(T1) = state1. The corresponding transition rule τ2 is defined as follows.
R
τ1
S1a
C1
B1
S1b
C1
B2
S1c
C2
S1cs
S2 τ2
τ3
S3a S3b
C3
B3
C4
S3bs
S4 τ4
τ5 C5
B4
Figure 5.2: Formal fault tree of hazard collision based on OTS
τ2 : level(T1) = state1 => level(T1) =state2 And from τ2, we get a sub-event S2 as follows.
S2 : level(T1) =state1∧bar =open
Notice here we should use a edge rather than a logic gate to connect S1cs and S2, and the transition ruleτ2 should also be labeled besides the edge for revising.
Further analysis will try to regress level(T1) = state1, and we would get a tran-sition as follows, that is, if a train has sent a ‘secure’ signal to the level crossing (de-noted by pos(T1) = sect1), and there is no radio communication error (denoted by
¬err-comm(T1)), and the barriers are open (denoted by bar = open), the crossing will accept this request (notice here bar =open is regarded as shared variable to ensure that there is no train on the crossing at this moment, which is equal to the variableIdling(sys) discussed in Section 3.2.2).
pos(T1) =sect1∧ ¬err-comm(T1)∧bar =open=> level(T1) =state1
However, based on the system design knowledge, we know that once the crossing has accepted a ‘secure’ request, then it must close the barriers until it gets a ‘passed’ signal from the train. In other words, A=> qβ with respect to S2, which violates the constraint of the transition rule. Therefore, we should focus on bar = open and derive another transition rule as follows.
τ3 : timeout(S, T2)∨pos(S, T2) =sect2∧ ¬err-comm(S, T2) => bar(S) = open
which states that two possibilities for the barriers to open are either a time-out event timeout(T2) (the crossing has been closed and waiting for a ‘passed’ signal over a designed time d, and then opens the barriers to protect cars against endless waiting) occurs, or another train T2 sends a ‘passed’ signal (denoted by pos(T2) = sect2) and there is no radio communication error (denoted by ¬err-comm(T2)). Use this transition rule to regress S2, we get two corresponding sub-events connected by an T-OR-gate below.
S3a : level(T1) =state1∧timeout(T2)
S3b : level(T1) = state1∧pos(T2) =sect2∧ ¬err-comm(T2)
Notice here a subtle system safety design issues is exposed by S3b, which states that the two events, level(T1) = state1 and pos(T2) =sect2 can not occur simultaneously, in other words, if the crossing confirm and accepts a ‘secure’ request from one train, it can not receive a ‘passed’ signal from another train at this moment.
Keep doing analysis in the similar way, finally we derive all the transition rules and events as follows, and the entire fault tree is shown in Figure 5.2. And for better under-standing, we list the explanation of the observations and events in Tabel 5.1.
B3 : timeout(T2) C3 : level(T1) = state1
Observation Values Explanation
pos(T1) sect1
A train has sent a ‘secure’ signal to the level cross-ing and is waitcross-ing for the ‘release’ signal before the crossing track segment.
crossing After getting the ‘release’ signal, a train is passing on the crossing
sect2 A train has passed the crossing and sent a ‘passed’
signal to the level crossing.
level(T1) state1 The level crossing has accepted a ‘secure’ request from a train.
state2 The level crossing has sent a ‘release’ permission to a train.
bar open The barriers are open.
close The barriers are close.
signal-bypass(T1) Boolean The driver of a train bypasses a ‘stop’ signal and enters the level crossing illegally.
err-brake(T1) Boolean The brake of a train is broken.
timeout(T1) Boolean A time-out fault occurs.
err-comm(T1) Boolean A radio communication error occurs between the level crossing and a train.
Table 5.1: Illustration of observations and events
S3bs : level(T1) = state1∧pos(T2) =sect2 C4 : ¬err-comm(T2)
τ4 : pos(T2) =crossing => pos(T2) = sect2 S4 : level(T1) =state1∧pos(T2) = crossing
τ5 : pos(T1) =sect1∧ ¬err-comm(T1)∧bar =open=> level(T1) =state1 B4 : bar =open∧pos(T2) =crossing
C5 : pos(T1) =sect1∧ ¬err-comm(T1)
It should be noted that as for S4, we focused on level(T1) = state1 instead of pos(T2) = crossing because we have found the transition rule for pos(T1) = crossing before (Notice here T1 and T2 are just variables denoting different trains, so the above two formulas/events can be understood as the same). An subtle issue is that finally we get B4, which is equal to the Root node, R, i.e., pos(T1) =crossing∧bar =open. Here, an important system safety issue was disclosed, that is, the fault events linked on the branch from R to B4 are mutual dependent (shown in Figure 5.2). And in contrast, the corresponding safety properties or invariants (the negations of the fault events which are related to system design compared with those fault events linked on the other branches) are alsomutual dependent.
Therefore, from Figure 5.2, we can get the following important information, while most of them are difficult to find by tradition FTA.
• Three basic events, signal-bypass(T1), err-brake(T1), and timeout(T1) should be taken into account with respect to hazard collision, and their corresponding condi-tions (CONDITIONING-events connected with the corresponding INHIBIT-gates) are also useful for taking precautions.
• Somemutual exclusion problems have been discovered , such as the eventS4, which states that when a train on the crossing, the crossing can not responds a ‘secure’
request from another train.
• Anmutual dependency relation between the fault events has been discovered, which has also been demonstrated in our formal verification in the last Chapter.
• All the transition rules founded in FTA can be reused in subsequent system formal modeling and verifying, together with deep understanding of the system and pri-mary design scheme followed by the stepwise and instructive fault tree construction processes.
• Last but not least, the correctness and completeness of the fault tree are guaranteed by the transition rules, which makes it possible to revise and recheck the fault tree in a easy and instructive way.