BDD卷土重来：静态与动态故障树的高效分析
软件工程
2022-03-29 v2
摘要
故障树是可靠性分析中的关键模型。经典的静态故障树(SFT)最好使用二元决策图(BDD)进行分析。基于状态的技术更适用于更具表达力的动态故障树(DFT)。本文遵循Dugan的方法，将两者的优势结合：动态子树通过模型检验马尔可夫模型进行分析，并替换为捕获所得失效概率的基本事件。所得SFT随后通过BDD进行分析。我们在Storm模型检验器中实现了该方法。大量实验(a)将我们基于纯BDD的SFT分析与多种现有SFT分析工具进行比较，(b)表明了我们的高效计算对多个时间点和平均失效时间评估的益处，以及(c)显示我们对Dugan方法的实现显著优于纯马尔可夫的DFT分析。我们的实现Storm-dft是目前唯一支持SFT和DFT高效分析的工具。
引用
@article{arxiv.2202.02829,
title = {BDDs Strike Back: Efficient Analysis of Static and Dynamic Fault Trees},
author = {Daniel Basgöze and Matthias Volk and Joost-Pieter Katoen and Shahid Khan and Marielle Stoelinga},
journal= {arXiv preprint arXiv:2202.02829},
year = {2022}
}
备注
Extended version of NFM'22 paper