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

Abstract

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
PublisherSpringer
Pages713-732
Number of pages20
ISBN (Electronic)978-3-031-06773-0
ISBN (Print)978-3-031-06772-3
DOIs
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
Volume13260
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference14th International Symposium NASA Formal Methods, NFM 2022
Abbreviated titleNFM 2022
Country/TerritoryUnited States
CityPasadena
Period24/05/2227/05/22

Fingerprint

Dive into the research topics of 'BDDs Strike Back: Efficient Analysis of Static and Dynamic Fault Trees'. Together they form a unique fingerprint.

Cite this