BDDs Strike Back: Efficient Analysis of Static and Dynamic Fault Trees

Daniel Basgöze, Matthias Volk, Joost-Pieter Katoen, Shahid Khan, Marielle Stoelinga

Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review

1 Citation (Scopus)
20 Downloads (Pure)


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.
Original languageEnglish
Title of host publicationNASA Formal Method
Subtitle of host publication14th International Symposium, NFM 2022, Pasadena, CA, USA, May 24–27, 2022, Proceedings
EditorsJyotirmoy V. Deshmukh, Klaus Havelund, Ivan Perez
Number of pages20
ISBN (Electronic)978-3-031-06773-0
ISBN (Print)978-3-031-06772-3
Publication statusPublished - 20 May 2022
Event14th International Symposium NASA Formal Methods, NFM 2022 - Pasadena, United States
Duration: 24 May 202227 May 2022
Conference number: 14

Publication series

NameLecture notes in computer science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference14th International Symposium NASA Formal Methods, NFM 2022
Abbreviated titleNFM 2022
Country/TerritoryUnited States


  • This work was part of the MISSION (Models in Space Systems: Integration, Operation, and Networking) project, funded by the European Union’s Horizon 2020 research and innovation programme under Marie Skłodowska-Curie Actions grant number 101008233.
  • 22/4 OA procedure

Cite this