Fault Trees on a Diet

Fault trees are a popular industrial technique for reliability modelling and analysis.  Their extension with common reliability patterns, such as spare management, functional dependencies, and sequencing — known as dynamic fault trees (DFTs) — has an adverse effect on scalability, prohibiting the analysis of complex, industrial cases by, e.g., probabilistic model checkers.  This paper presents a novel, fully automated reduction technique for DFTs.  The key idea is to interpret DFTs as directed graphs and exploit graph rewriting to simplify them.  We present a collection of rewrite rules, address their correctness, and give a simple heuristic to determine the order of rewriting.  Experiments on a large set of benchmarks show substantial fault tree simplifications, yielding state space reductions and timing gains of up to two orders of magnitude.

People Involved

Sebastian Junges, Dennis Guck, Joost-Pieter Katoen, Arend Rensink, Mariëlle Stoelinga

Further information

A paper presenting the results is accepted for publication at SETTA’15.

The presented results are also contained in Sebastian Junges’ master thesis, including a full background on semantics and rewriting. An overview of the rules by name – with a listing where to find them in the master thesis can be found here.

Tool chain

The rewriting tool-chain is available either via

  • a modified Debian-ISO for use in a virtual machine (Installs Debian 8.0 with all dependencies and the tool chain) Notice that Groove *currently* only works if the virtual machine has at least two processors available, or
  • as a zip-archive. (Tested on Linux and Mac OS).

DFTCalc is available either via a web-interface or as a download (instructions).
Due to license restrictions of CADP, we can not distribute DFTCalc together with the other parts of the rewrite tool-chain.

Benchmarks

Detailed benchmark results can be found in this overview – it contains a full table of all benchmarks, an indication which benchmarks are depicted in Figure 9 and more figures which illustrate the effect of the rewriting on scalability.
Benchmark files are available for benchmarks and are available from the virtual disk image. The benchmark files include all benchmarks from the
HECS, MCS, RC, SF suite, as well as the SAP and HCAS examples. For each benchmark instance, we provide (a) the  generated fault tree, (b) the normalized fault tree (c) the simplified fault tree.