Running Storm on DFTs
Table of contents
Analyzing DFTs
The support for fault tree analysis is bundled in the storm-dft binary which should be created during the build. The input of Dynamic fault trees (DFTs) is given in the Galileo format.
Example 1 (Fault tree analysis of a motorbike)
We consider the example of a motorbike with a front wheel and a rear wheel. When one of the wheels fails, the spare wheel can be used as a replacement. If more than one wheel fails, the whole motorbike fails. The fault tree for the motor bike is given in the following.
Download DFT file of motorbike
toplevel "Bike";
"Bike" or "Front" "Back";
"Front" wsp "FrontWheel" "SpareWheel";
"Back" wsp "RearWheel" "SpareWheel";
"FrontWheel" lambda=0.5 dorm=0.0;
"RearWheel" lambda=0.5 dorm=0.0;
"SpareWheel" lambda=1.0 dorm=0.1;
For the fault tree analysis two measures are of importance: reliability and mean-time-to-failure (MTTF). The reliability at time t=1 can be computed with the following call:
$ storm-dft -dft motorbike.dft --timebound 1
Storm-DyFTeE 1.0.0
Command line arguments: -dft motorbike.dft --timebound 1
Current working directory: ~/storm/storm/build/bin
Loading DFT from file motorbike.dft
--------------------------------------------------------------
Model type: CTMC (sparse)
States: 10
Transitions: 15
Reward Models: none
Labels: 2
* init -> 1 state(s)
* failed -> 6 state(s)
choice labels: no
--------------------------------------------------------------
Model checking property Pmin=? [true U<=1 "failed"] ...
Result (initial states): 0.3577681657
Time for model checking: 0.000s.
Times:
Exploration: 0.001s
Building: 0.000s
Bisimulation: 0.000s
Modelchecking: 0.000s
Total: 0.001s
Result: [0.3577681657]
At time t=1 the probability of having a failure of the motorbike is 35.78%.
For a better indication of the reliability over time multiple time points can be computed at once:
$ storm-dft -dft motorbike.dft --timepoints 1 5 0.1
Storm-DyFTeE 1.0.0
Command line arguments: -dft motorbike.dft --timepoints 1 5 0.1
Current working directory: ~/storm/build/bin
Loading DFT from file motorbike.dft
--------------------------------------------------------------
Model type: CTMC (sparse)
States: 10
Transitions: 15
Reward Models: none
Labels: 2
* init -> 1 state(s)
* failed -> 6 state(s)
choice labels: no
--------------------------------------------------------------
Model checking property Pmin=? [true U<=1 "failed"] ...
Result (initial states): 0.3577681657
Time for model checking: 0.000s.
Model checking property Pmin=? [true U<=11/10 "failed"] ...
Result (initial states): 0.4017604598
Time for model checking: 0.000s.
Model checking property Pmin=? [true U<=6/5 "failed"] ...
Result (initial states): 0.4442146745
Time for model checking: 0.000s.
Model checking property Pmin=? [true U<=13/10 "failed"] ...
Result (initial states): 0.4848810529
Time for model checking: 0.000s.
Model checking property Pmin=? [true U<=7/5 "failed"] ...
Result (initial states): 0.523591286
Time for model checking: 0.000s.
Model checking property Pmin=? [true U<=3/2 "failed"] ...
Result (initial states): 0.5602431065
Time for model checking: 0.000s.
Model checking property Pmin=? [true U<=8/5 "failed"] ...
Result (initial states): 0.5947861527
Time for model checking: 0.000s.
Model checking property Pmin=? [true U<=17/10 "failed"] ...
Result (initial states): 0.6272113724
Time for model checking: 0.000s.
Model checking property Pmin=? [true U<=9/5 "failed"] ...
Result (initial states): 0.6575417607
Time for model checking: 0.000s.
Model checking property Pmin=? [true U<=19/10 "failed"] ...
Result (initial states): 0.6858242617
Time for model checking: 0.000s.
Model checking property Pmin=? [true U<=2 "failed"] ...
Result (initial states): 0.7121244631
Time for model checking: 0.000s.
Model checking property Pmin=? [true U<=21/10 "failed"] ...
Result (initial states): 0.7365207031
Time for model checking: 0.000s.
Model checking property Pmin=? [true U<=11/5 "failed"] ...
Result (initial states): 0.7591006077
Time for model checking: 0.000s.
Model checking property Pmin=? [true U<=23/10 "failed"] ...
Result (initial states): 0.7799576577
Time for model checking: 0.000s.
Model checking property Pmin=? [true U<=12/5 "failed"] ...
Result (initial states): 0.7991881066
Time for model checking: 0.000s.
Model checking property Pmin=? [true U<=5/2 "failed"] ...
Result (initial states): 0.816889687
Time for model checking: 0.000s.
Model checking property Pmin=? [true U<=13/5 "failed"] ...
Result (initial states): 0.8331592523
Time for model checking: 0.000s.
Model checking property Pmin=? [true U<=27/10 "failed"] ...
Result (initial states): 0.8480920639
Time for model checking: 0.000s.
Model checking property Pmin=? [true U<=14/5 "failed"] ...
Result (initial states): 0.861780707
Time for model checking: 0.000s.
Model checking property Pmin=? [true U<=29/10 "failed"] ...
Result (initial states): 0.8743140803
Time for model checking: 0.000s.
Model checking property Pmin=? [true U<=3 "failed"] ...
Result (initial states): 0.8857774128
Time for model checking: 0.000s.
Model checking property Pmin=? [true U<=31/10 "failed"] ...
Result (initial states): 0.8962517674
Time for model checking: 0.000s.
Model checking property Pmin=? [true U<=16/5 "failed"] ...
Result (initial states): 0.9058135182
Time for model checking: 0.000s.
Model checking property Pmin=? [true U<=33/10 "failed"] ...
Result (initial states): 0.9145347989
Time for model checking: 0.000s.
Model checking property Pmin=? [true U<=17/5 "failed"] ...
Result (initial states): 0.9224833027
Time for model checking: 0.000s.
Model checking property Pmin=? [true U<=7/2 "failed"] ...
Result (initial states): 0.9297220126
Time for model checking: 0.000s.
Model checking property Pmin=? [true U<=18/5 "failed"] ...
Result (initial states): 0.9363098495
Time for model checking: 0.000s.
Model checking property Pmin=? [true U<=37/10 "failed"] ...
Result (initial states): 0.942301609
Time for model checking: 0.000s.
Model checking property Pmin=? [true U<=19/5 "failed"] ...
Result (initial states): 0.9477478148
Time for model checking: 0.000s.
Model checking property Pmin=? [true U<=39/10 "failed"] ...
Result (initial states): 0.9526954318
Time for model checking: 0.000s.
Model checking property Pmin=? [true U<=4 "failed"] ...
Result (initial states): 0.9571878562
Time for model checking: 0.000s.
Model checking property Pmin=? [true U<=41/10 "failed"] ...
Result (initial states): 0.9612648229
Time for model checking: 0.000s.
Model checking property Pmin=? [true U<=21/5 "failed"] ...
Result (initial states): 0.964963109
Time for model checking: 0.000s.
Model checking property Pmin=? [true U<=43/10 "failed"] ...
Result (initial states): 0.9683165348
Time for model checking: 0.000s.
Model checking property Pmin=? [true U<=22/5 "failed"] ...
Result (initial states): 0.9713558929
Time for model checking: 0.000s.
Model checking property Pmin=? [true U<=9/2 "failed"] ...
Result (initial states): 0.974109601
Time for model checking: 0.000s.
Model checking property Pmin=? [true U<=23/5 "failed"] ...
Result (initial states): 0.9766036105
Time for model checking: 0.000s.
Model checking property Pmin=? [true U<=47/10 "failed"] ...
Result (initial states): 0.9788617753
Time for model checking: 0.000s.
Model checking property Pmin=? [true U<=24/5 "failed"] ...
Result (initial states): 0.9809055689
Time for model checking: 0.000s.
Model checking property Pmin=? [true U<=49/10 "failed"] ...
Result (initial states): 0.9827548586
Time for model checking: 0.000s.
Model checking property Pmin=? [true U<=5 "failed"] ...
Result (initial states): 0.9844277921
Time for model checking: 0.000s.
Times:
Exploration: 0.001s
Building: 0.000s
Bisimulation: 0.000s
Modelchecking: 0.006s
Total: 0.007s
Result: [0.3577681657, 0.4017604598, 0.4442146745, 0.4848810529, 0.523591286, 0.5602431065, 0.5947861527, 0.6272113724, 0.6575417607, 0.6858242617, 0.7121244631, 0.7365207031, 0.7591006077, 0.7799576577, 0.7991881066, 0.816889687, 0.8331592523, 0.8480920639, 0.861780707, 0.8743140803, 0.8857774128, 0.8962517674, 0.9058135182, 0.9145347989, 0.9224833027, 0.9297220126, 0.9363098495, 0.942301609, 0.9477478148, 0.9526954318, 0.9571878562, 0.9612648229, 0.964963109, 0.9683165348, 0.9713558929, 0.974109601, 0.9766036105, 0.9788617753, 0.9809055689, 0.9827548586, 0.9844277921]
Here the reliability for all time points \(1+i\cdot0.1, i \in \{0, ..., 40\}\) is computed.
The second measure MTTF computes the expected time of the failure of the motorbike.
$ storm-dft -dft motorbike.dft -mttf
Storm-DyFTeE 1.0.0
Command line arguments: -dft motorbike.dft -mttf
Current working directory: ~/storm/build/bin
Loading DFT from file motorbike.dft
--------------------------------------------------------------
Model type: CTMC (sparse)
States: 10
Transitions: 15
Reward Models: none
Labels: 2
* init -> 1 state(s)
* failed -> 6 state(s)
choice labels: no
--------------------------------------------------------------
Model checking property T[exp]min=? [F "failed"] ...
Result (initial states): 1.606060606
Time for model checking: 0.000s.
Times:
Exploration: 0.001s
Building: 0.000s
Bisimulation: 0.000s
Modelchecking: 0.000s
Total: 0.002s
Result: [1.606060606]
The motorbike has an expected lifetime of 1.61.
Example 2 (Fault tree analysis of the Hypothetical Example Computer System (HECS))
In this example we consider the Hypothetical Example Computer System (HECS) from the NASA handbook on fault trees. It models a computer system consisting of a processor unit with two processors and a spare processor, a memory unit with 5 memory slots, an operator interface consisting of hardware and software, and a 2-redundant bus.
toplevel "System";
"System" or "PSF" "MSF" "BSF" "IF";
"PSF" and "P_1" "P_2";
"P_1" wsp "A_1" "A_S";
"P_2" wsp "A_2" "A_S";
"A_1" lambda=1.0e-3 dorm=0;
"A_2" lambda=1.0e-3 dorm=0;
"A_S" lambda=1.0e-3 dorm=0;
"MSF" 3of5 "M_1" "M_2" "M_3" "M_4" "M_5";
"M_1" lambda=6.0e-4 dorm=0;
"M_2" lambda=6.0e-4 dorm=0;
"M_3" lambda=6.0e-4 dorm=0;
"M_4" lambda=6.0e-4 dorm=0;
"M_5" lambda=6.0e-4 dorm=0;
"BSF" and "BUS_1" "BUS_2";
"BUS_1" lambda=1.0e-5 dorm=0;
"BUS_2" lambda=1.0e-5 dorm=0;
"IF" or "HW" "SW";
"HW" lambda=5.0e-4 dorm=0;
"SW" lambda=6.0e-4 dorm=0;
We compute the MTTF again.
$ storm-dft -dft hecs.dft -mttf
Storm-DyFTeE 1.0.0
Command line arguments: -dft hecs.dft -mttf
Current working directory: ~/storm/build/bin
Loading DFT from file hecs.dft
--------------------------------------------------------------
Model type: CTMC (sparse)
States: 1426
Transitions: 3845
Reward Models: none
Labels: 2
* init -> 1 state(s)
* failed -> 1090 state(s)
choice labels: no
--------------------------------------------------------------
Model checking property T[exp]min=? [F "failed"] ...
Result (initial states): 573.7440971
Time for model checking: 0.003s.
Times:
Exploration: 0.015s
Building: 0.000s
Bisimulation: 0.000s
Modelchecking: 0.003s
Total: 0.019s
Result: [573.7440971]
As the system is larger, it makes sense to use symmetry reduction as an optimization. This is enabled by default for all analyses and exploits symmetries in the system, for example stemming from redundant components. Symmetry reduction reduces the model size drastically which improves the analysis time.
For reliability another optimization can be enabled: modularisation via --modularisation.
$ storm-dft -dft hecs.dft --timebound 500 --modularisation
Storm-DyFTeE 1.0.0
Command line arguments: -dft hecs.dft --timebound 500 -symred --modularisation
Current working directory: ~/storm/build/bin
Loading DFT from file hecs.dft
--------------------------------------------------------------
Model type: CTMC (sparse)
States: 5
Transitions: 6
Reward Models: none
Labels: 2
* init -> 1 state(s)
* failed -> 1 state(s)
choice labels: no
--------------------------------------------------------------
Model checking property Pmin=? [true U<=500 "failed"] ...
Result (initial states): 0.0453951136
Time for model checking: 0.000s.
--------------------------------------------------------------
Model type: CTMC (sparse)
States: 2
Transitions: 2
Reward Models: none
Labels: 2
* init -> 1 state(s)
* failed -> 1 state(s)
choice labels: no
--------------------------------------------------------------
Model checking property Pmin=? [true U<=500 "failed"] ...
Result (initial states): 0.2591817412
Time for model checking: 0.000s.
--------------------------------------------------------------
Model type: CTMC (sparse)
States: 2
Transitions: 2
Reward Models: none
Labels: 2
* init -> 1 state(s)
* failed -> 1 state(s)
choice labels: no
--------------------------------------------------------------
Model checking property Pmin=? [true U<=500 "failed"] ...
Result (initial states): 0.2591817412
Time for model checking: 0.000s.
--------------------------------------------------------------
Model type: CTMC (sparse)
States: 2
Transitions: 2
Reward Models: none
Labels: 2
* init -> 1 state(s)
* failed -> 1 state(s)
choice labels: no
--------------------------------------------------------------
Model checking property Pmin=? [true U<=500 "failed"] ...
Result (initial states): 0.2591817412
Time for model checking: 0.000s.
--------------------------------------------------------------
Model type: CTMC (sparse)
States: 2
Transitions: 2
Reward Models: none
Labels: 2
* init -> 1 state(s)
* failed -> 1 state(s)
choice labels: no
--------------------------------------------------------------
Model checking property Pmin=? [true U<=500 "failed"] ...
Result (initial states): 0.2591817412
Time for model checking: 0.000s.
--------------------------------------------------------------
Model type: CTMC (sparse)
States: 2
Transitions: 2
Reward Models: none
Labels: 2
* init -> 1 state(s)
* failed -> 1 state(s)
choice labels: no
--------------------------------------------------------------
Model checking property Pmin=? [true U<=500 "failed"] ...
Result (initial states): 0.2591817412
Time for model checking: 0.000s.
--------------------------------------------------------------
Model type: CTMC (sparse)
States: 2
Transitions: 2
Reward Models: none
Labels: 2
* init -> 1 state(s)
* failed -> 1 state(s)
choice labels: no
--------------------------------------------------------------
Model checking property Pmin=? [true U<=500 "failed"] ...
Result (initial states): 0.004987498783
Time for model checking: 0.000s.
--------------------------------------------------------------
Model type: CTMC (sparse)
States: 2
Transitions: 2
Reward Models: none
Labels: 2
* init -> 1 state(s)
* failed -> 1 state(s)
choice labels: no
--------------------------------------------------------------
Model checking property Pmin=? [true U<=500 "failed"] ...
Result (initial states): 0.004987498783
Time for model checking: 0.000s.
--------------------------------------------------------------
Model type: CTMC (sparse)
States: 2
Transitions: 2
Reward Models: none
Labels: 2
* init -> 1 state(s)
* failed -> 1 state(s)
choice labels: no
--------------------------------------------------------------
Model checking property Pmin=? [true U<=500 "failed"] ...
Result (initial states): 0.2211992058
Time for model checking: 0.000s.
--------------------------------------------------------------
Model type: CTMC (sparse)
States: 2
Transitions: 2
Reward Models: none
Labels: 2
* init -> 1 state(s)
* failed -> 1 state(s)
choice labels: no
--------------------------------------------------------------
Model checking property Pmin=? [true U<=500 "failed"] ...
Result (initial states): 0.2591817412
Time for model checking: 0.000s.
Times:
Exploration: 0.006s
Building: 0.000s
Bisimulation: 0.000s
Modelchecking: 0.001s
Total: 0.009s
Result: [0.5117286837]
Here independent subtrees are analyzed separately and the results are combined yielding the total reliability.