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

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

doi:10.1007/978-3-031-06773-0_38

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 proceeding › Chapter › Academic › peer-review

11 Citations (Scopus)

297 Downloads (Pure)

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 language	English
Title of host publication	NASA Formal Method
Subtitle of host publication	14th International Symposium, NFM 2022, Pasadena, CA, USA, May 24–27, 2022, Proceedings
Editors	Jyotirmoy V. Deshmukh, Klaus Havelund, Ivan Perez
Publisher	Springer
Pages	713-732
Number of pages	20
ISBN (Electronic)	978-3-031-06773-0
ISBN (Print)	978-3-031-06772-3
DOIs	https://doi.org/10.1007/978-3-031-06773-0_38
Publication status	Published - 20 May 2022
Event	14th International Symposium NASA Formal Methods, NFM 2022 - Pasadena, United States Duration: 24 May 2022 → 27 May 2022 Conference number: 14

Publication series

Name	Lecture notes in computer science
Volume	13260
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	14th International Symposium NASA Formal Methods, NFM 2022
Abbreviated title	NFM 2022
Country/Territory	United States
City	Pasadena
Period	24/05/22 → 27/05/22

Keywords

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

Access to Document

10.1007/978-3-031-06773-0_38

2202.02829Submitted version, 697 KB
ArticleFinal published version, 470 KBLicence: Taverne

Cite this

Basgöze, D., Volk, M., Katoen, J.-P., Khan, S., & Stoelinga, M. (2022). BDDs Strike Back: Efficient Analysis of Static and Dynamic Fault Trees. In J. V. Deshmukh, K. Havelund, & I. Perez (Eds.), NASA Formal Method: 14th International Symposium, NFM 2022, Pasadena, CA, USA, May 24–27, 2022, Proceedings (pp. 713-732). Article Chapter 38 (Lecture notes in computer science; Vol. 13260). Springer. https://doi.org/10.1007/978-3-031-06773-0_38

Basgöze, Daniel ; Volk, Matthias ; Katoen, Joost-Pieter et al. / BDDs Strike Back : Efficient Analysis of Static and Dynamic Fault Trees. NASA Formal Method: 14th International Symposium, NFM 2022, Pasadena, CA, USA, May 24–27, 2022, Proceedings. editor / Jyotirmoy V. Deshmukh ; Klaus Havelund ; Ivan Perez. Springer, 2022. pp. 713-732 (Lecture notes in computer science).

@inbook{cfedfca7e9d54933b38793002ec667d3,

title = "BDDs Strike Back: Efficient Analysis of Static and Dynamic Fault Trees",

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{\textquoteright}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{\textquoteright}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.",

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

author = "Daniel Basg{\"o}ze and Matthias Volk and Joost-Pieter Katoen and Shahid Khan and Marielle Stoelinga",

note = "Funding Information: This work has been partially funded by NWO under the grant PrimaVera number NWA.1160.18.238, European Union{\textquoteright}s Horizon 2020 research and innovation programme under the Marie Sk lodowska-Curie grant agreement No. 101008233 (Mission), and the ERC Consolidator Grant 864075 (CAESAR). Khan is funded by a HEC-DAAD stipend. Publisher Copyright: {\textcopyright} 2022, Springer Nature Switzerland AG.; 14th International Symposium NASA Formal Methods, NFM 2022, NFM 2022 ; Conference date: 24-05-2022 Through 27-05-2022",

year = "2022",

month = may,

day = "20",

doi = "10.1007/978-3-031-06773-0\_38",

language = "English",

isbn = "978-3-031-06772-3",

series = "Lecture notes in computer science",

publisher = "Springer",

pages = "713--732",

editor = "Deshmukh, \{Jyotirmoy V.\} and Klaus Havelund and Ivan Perez",

booktitle = "NASA Formal Method",

address = "Germany",

}

Basgöze, D, Volk, M, Katoen, J-P, Khan, S & Stoelinga, M 2022, BDDs Strike Back: Efficient Analysis of Static and Dynamic Fault Trees. in JV Deshmukh, K Havelund & I Perez (eds), NASA Formal Method: 14th International Symposium, NFM 2022, Pasadena, CA, USA, May 24–27, 2022, Proceedings., Chapter 38, Lecture notes in computer science, vol. 13260, Springer, pp. 713-732, 14th International Symposium NASA Formal Methods, NFM 2022, Pasadena, California, United States, 24/05/22. https://doi.org/10.1007/978-3-031-06773-0_38

BDDs Strike Back: Efficient Analysis of Static and Dynamic Fault Trees. / Basgöze, Daniel; Volk, Matthias; Katoen, Joost-Pieter et al.
NASA Formal Method: 14th International Symposium, NFM 2022, Pasadena, CA, USA, May 24–27, 2022, Proceedings. ed. / Jyotirmoy V. Deshmukh; Klaus Havelund; Ivan Perez. Springer, 2022. p. 713-732 Chapter 38 (Lecture notes in computer science; Vol. 13260).

Research output: Chapter in Book/Report/Conference proceeding › Chapter › Academic › peer-review

TY - CHAP

T1 - BDDs Strike Back

T2 - 14th International Symposium NASA Formal Methods, NFM 2022

AU - Basgöze, Daniel

AU - Volk, Matthias

AU - Katoen, Joost-Pieter

AU - Khan, Shahid

AU - Stoelinga, Marielle

N1 - Conference code: 14

PY - 2022/5/20

Y1 - 2022/5/20

N2 - 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.

AB - 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.

KW - 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.

KW - 22/4 OA procedure

UR - https://arxiv.org/abs/2202.02829

U2 - 10.1007/978-3-031-06773-0_38

DO - 10.1007/978-3-031-06773-0_38

M3 - Chapter

SN - 978-3-031-06772-3

T3 - Lecture notes in computer science

SP - 713

EP - 732

BT - NASA Formal Method

A2 - Deshmukh, Jyotirmoy V.

A2 - Havelund, Klaus

A2 - Perez, Ivan

PB - Springer

Y2 - 24 May 2022 through 27 May 2022

ER -

Basgöze D, Volk M, Katoen JP, Khan S, Stoelinga M. BDDs Strike Back: Efficient Analysis of Static and Dynamic Fault Trees. In Deshmukh JV, Havelund K, Perez I, editors, NASA Formal Method: 14th International Symposium, NFM 2022, Pasadena, CA, USA, May 24–27, 2022, Proceedings. Springer. 2022. p. 713-732. Chapter 38. (Lecture notes in computer science). doi: 10.1007/978-3-031-06773-0_38

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

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Artifact for "BDDs Strike Back - Efficient Analysis of Static and Dynamic Fault Trees"