论文标题
BDDS反击：有效分析静态和动态故障树
BDDs Strike Back: Efficient Analysis of Static and Dynamic Fault Trees
论文作者
论文摘要
故障树是可靠性分析中的关键模型。最好使用二进制决策图（BDD）分析经典的静态断层树（SFT）。基于国家的技术有利于更具表现力的动态断层树（DFT）。本文通过遵循Dugan的方法结合了两全其美的最佳：通过模型检查Markov模型，分析了动态子树，并由捕获获得的故障概率的基本事件取代。然后通过BDD分析所得的SFT。我们在风暴模型检查器中实现了这种方法。广泛的实验（a）将我们基于BDD的SFT分析与各种现有的SFT分析工具进行比较，（b）表明我们有效计算对多个时间点的好处以及对平均时间到失败的评估，（c）表明，我们对Dugan方法的实施极大地超过了DFTS的Markovian分析。目前，我们的实施风暴-DFT是支持SFT和DFT的有效分析的唯一工具。
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.
