Safety-critical infrastructures must operate in a safe and reliable way. Fault tree analysis is a widespread method used for risk assessment of these systems: fault trees (FTs) are required by, e.g., the Federal Aviation Administration and the Nuclear Regulatory Commission. In spite of their popularity, little work has been done on formulating structural queries about FTs and analyzing these, e.g., when evaluating potential scenarios, and to give practitioners instruments to formulate queries on FTs in an understandable yet powerful way. In this paper, we aim to fill this gap by extending BFL, a logic that reasons about Boolean FTs. To do so, we introduce a Probabilistic Fault tree Logic (PFL). PFL is a simple, yet expressive logic that supports easier formulation of complex scenarios and specification of FT properties that comprise probabilities. Alongside PFL, we present LangPFL, a domain specific language to further ease property specification. We showcase PFL and LangPFL by applying them to a COVID-19 related FT and to a FT for an oil/gas pipeline. Finally, we present theory and model checking algorithms based on binary decision diagrams (BDDs).
More recent news
- Fri 26 May 2023ZORRO project Kick-off meeting 25 May 2023
- Tue 2 May 2023Joost-Pieter Katoen and former FMT-colleague Holger Hermanns and co-authors receive the 2023 Jean-Claude Laprie Award in Dependable Computing
- Fri 21 Apr 2023FMT welcomes three MISSION visitors
- Fri 31 Mar 2023Inter-Actief Teacher's award for Tom van Dijk!
- Fri 24 Mar 2023Paper accepted (Milan Lopuhaä, Marielle Stoelinga)