Abstract:
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).
Monday 28 November 2022
More recent news
- Tue 23 Apr 20242nd place of student teams at VerifyThis 2024
- Tue 9 Apr 2024Papers of the Month: April 2024
- Wed 27 Mar 2024Faizan Ahmed appointed Programme Director BIT
- Tue 12 Mar 2024FMT Papers of the Month: March 2024
- Tue 27 Feb 2024Tom van Dijk in live broadcast: 'AI in Education'