BDDs Strike Back: Efficient Analysis of Static and Dynamic Fault Trees
This work addresses reliability analysis for engineers and researchers by providing an incremental improvement in computational efficiency for fault tree analysis.
The paper tackles the problem of efficiently analyzing static and dynamic fault trees for reliability analysis by combining binary decision diagrams (BDD) for static parts and model checking for dynamic parts, implemented in the Storm model checker. The result shows that their implementation significantly outperforms pure Markovian analysis for dynamic fault trees and is the only tool supporting efficient analysis for both types.
Fault trees are a key model in reliability analysis. Classical static fault trees (SFT) can best be analysed using binary decision diagrams (BDD). State-based techniques are favorable for the more expressive dynamic fault trees (DFT). This paper combines the best of both worlds by following Dugan's approach: dynamic sub-trees are analysed via model checking Markov models and replaced by basic events capturing the obtained failure probabilities. The resulting SFT is then analysed via BDDs. We implemented this approach in the Storm model checker. Extensive experiments (a) compare our pure BDD-based analysis of SFTs to various existing SFT analysis tools, (b) indicate the benefits of our efficient calculations for multiple time points and the assessment of the mean-time-to-failure, and (c) show that our implementation of Dugan's approach significantly outperforms pure Markovian analysis of DFTs. Our implementation Storm-dft is currently the only tool supporting efficient analysis for both SFTs and DFTs.