RES for non-Markovian repairable fault trees
473
butions of BEs/SBEs, imprinting this information in the thresholds k . Several
algorithms can do such selection of thresholds. They operate sequentially, starting from the initial state—a fully operational tree—which has importance i 0 = 0.
For instance, Expected Success [10] runs N finite-life simulations. If K <
N
2 simulations reach the next smallest importance i 1 > i 0 , then the first threshold will
be 1 = i 1 . Next, N simulations start from states with importance i 1 , to determine whether the next importance i 2 should be chosen as threshold 2 , and so on.
Expected Success also computes the effort per splitting region S k = {x ∈ S |
k+1 > I(x) k }. For Fixed Effort, “effort” is the base number of simulations
to run in region S k . For restart, it is the number of clones spawned when
threshold k+1 is up-crossed. In general, if K out of N pilot simulations make it
from k−1 to k , then the k-th effort is
N
K
. This is chosen so that, during res
estimations, one simulation makes it from threshold k−1 to k on average.
Thus, using the method from [11, 12] based on our importance function I ,
we compute (automatically) the thresholds and their effort for tree . This is all
the meta-information required to apply importance splitting res [19, 18, 11].
Importance function
¬
Property query (metric)
IOSA semantic model
RFT model
(extended
Galileo)
RFT ࡽ IOSA
converter
FIG
Fig. 4: Tool chain
Implementation. Fig. 4 outlines a tool chain implemented to deploy the theory described above. The input model is an rft, described in the Galileo textual
format [42, 41] extended with repairs and arbitrary pdfs. This rft file is given
as input to a Java converter that produces three outputs: the iosa semantics
of the tree, the property queries for its reliability or availability, and our compositional importance function in terms of variables of the iosa semantic model.
This information is dumped into a single text file and fed to FIG: a statistical
model checker specialised in importance splitting res. FIG interprets this importance function, deploying it into its internal model representation, which results
in a global function for the whole tree. FIG can then use isplit algorithms such
as restart and Fixed Effort, via the automatic methods described above. The
result are confidence intervals that estimate the reliability or availability of the
rft. In this way, we implemented automatic importance splitting for fta. In
[9] we provide more details about our tool chain and its capabilities.
5 Experimental evaluation
5.1 General setup
Using our tool chain, we computed the unreliability and unavailability of 26
highly-resilient repairable non-Markovian dfts. These trees come from seven
473
butions of BEs/SBEs, imprinting this information in the thresholds k . Several
algorithms can do such selection of thresholds. They operate sequentially, starting from the initial state—a fully operational tree—which has importance i 0 = 0.
For instance, Expected Success [10] runs N finite-life simulations. If K <
N
2 simulations reach the next smallest importance i 1 > i 0 , then the first threshold will
be 1 = i 1 . Next, N simulations start from states with importance i 1 , to determine whether the next importance i 2 should be chosen as threshold 2 , and so on.
Expected Success also computes the effort per splitting region S k = {x ∈ S |
k+1 > I(x) k }. For Fixed Effort, “effort” is the base number of simulations
to run in region S k . For restart, it is the number of clones spawned when
threshold k+1 is up-crossed. In general, if K out of N pilot simulations make it
from k−1 to k , then the k-th effort is
N
K
. This is chosen so that, during res
estimations, one simulation makes it from threshold k−1 to k on average.
Thus, using the method from [11, 12] based on our importance function I ,
we compute (automatically) the thresholds and their effort for tree . This is all
the meta-information required to apply importance splitting res [19, 18, 11].
Importance function
¬
Property query (metric)
IOSA semantic model
RFT model
(extended
Galileo)
RFT ࡽ IOSA
converter
FIG
Fig. 4: Tool chain
Implementation. Fig. 4 outlines a tool chain implemented to deploy the theory described above. The input model is an rft, described in the Galileo textual
format [42, 41] extended with repairs and arbitrary pdfs. This rft file is given
as input to a Java converter that produces three outputs: the iosa semantics
of the tree, the property queries for its reliability or availability, and our compositional importance function in terms of variables of the iosa semantic model.
This information is dumped into a single text file and fed to FIG: a statistical
model checker specialised in importance splitting res. FIG interprets this importance function, deploying it into its internal model representation, which results
in a global function for the whole tree. FIG can then use isplit algorithms such
as restart and Fixed Effort, via the automatic methods described above. The
result are confidence intervals that estimate the reliability or availability of the
rft. In this way, we implemented automatic importance splitting for fta. In
[9] we provide more details about our tool chain and its capabilities.
5 Experimental evaluation
5.1 General setup
Using our tool chain, we computed the unreliability and unavailability of 26
highly-resilient repairable non-Markovian dfts. These trees come from seven