RWTH Aachen University (GERMANY)
University of Twente (THE NETHERLANDS)
CADP (Construction and Analysis of Distributed Processes)
Fault tree analysis is one of the most prominent safety assessment
technique, standardised by the IEC and deployed by many companies
and institutions. Fault trees (FTs) model how failures propagate
through the system: FT leaves model component failures and are equipped
with continuous probability distributions; FT gates model how component
failures lead to system failures. Dynamic fault trees (DFTs) are a
well-known extension to standard fault trees that cater for common
dependability patterns, such as spare management, functional
dependency, and sequencing. Analysis of DFTs relies on extracting
an underlying stochastic model and analyzing it using stochastic model
checking. Since the order in which the DFT components fail matters,
this approach severely suffers from the state space explosion problem.
A novel technique is proposed to reduce the state space of DFTs prior to their analysis. The key idea is to consider DFTs as (typed) directed graphs and manipulate them by graph rewriting. The technique was implemented on top of the graph transformation tool GROOVE and the DFT analysis tool DFTCalc, yielding a fully automated tool chain for graph-based DFT reduction and analysis. The DFT is translated into the input format of GROOVE, which applies the graph rewriting rules defined for DFT reduction. The output of GROOVE (i.e., the rewritten graph), is translated back into a DFT that is then analysed by DFTCalc. DFTCalc exploits CADP for compositional state space generation and reduction (using bisimulation minimisation) of the underlying IMC of the DFT. Finally, the resulting Markov chain is analysed for the user-specified measure by the probabilistic model checker MRMC.
Several variations of seven benchmarks were analysed, comprised of over 170 fault trees in total, originating from standard examples from the literature as well as industrial case studies from aerospace and railway engineering. Rewriting enabled to cope with 49 DFTs that could not be handled before. For the other fault trees rewriting pays off, being much faster and more memory efficient, up to two orders of magnitude. This comes at no run-time penalty: graph rewriting is very fast and the stochastic model generation is significantly accelerated due to the DFT reduction.
The novel reduction technique for minimising DFTs using graph rewriting
yields drastic savings in terms of time and memory consumption (up to
two orders of magnitude). The rewriting approach is applicable too for
alternative DFT analysis techniques that isolate static sub-trees.
It is also applicable to trees similar to DFTs, e.g., dynamic
event/fault trees, extended FTs, and attack trees.
S. Junges, D. Guck, J-P. Katoen, A. Rensink, and M. Stoelinga.
"Fault Trees on a Diet - Automated Reduction by Graph Rewriting".
Proceedings of the 1st International Symposium on Dependable Software
Engineering: Theories, Tools, and Applications SETTA'2015,
LNCS vol. 9409, pages 3-18. Springer Verlag, November 2015.
Available on-line at: http://eprints.eemcs.utwente.nl/26418/01/chp%253A10.1007%252F978-3-319-25942-0_1.pdf
or from the VASY FTP site in PDF or PostScript
Formal Methods and Tools
Department of Computer Science
University of Twente
P.O. Box 217
NL-7500 AE Enschede
Tel: +31 (0)53 489 4862
|Further remarks:||This tool, amongst others, is described on the CADP Web Page: http://cadp.inria.fr|