BFL: a Logic to Reason about Fault Trees

Stefano M. Nicoletti, E. Moritz Hahn, Mariëlle I.A. Stoelinga

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Abstract

Safety-critical infrastructures must operate safely and reliably. Fault tree analysis is a widespread method used to assess risks in these systems: fault trees (FTs) are required — among others — by the Federal Aviation Authority, the Nuclear Regulatory Commission, in the ISO26262 standard for autonomous driving and for software development in aerospace systems. Although popular both in industry and academia, FTs lack a systematic way to formulate powerful and understandable analysis queries. In this paper, we aim to fill this gap and introduce Boolean Fault tree Logic (BFL), a logic to reason about FTs. BFL is a simple, yet expressive logic that supports easier formulation of complex scenarios and specification of FT properties. Alongside BFL, we present model checking algorithms based on binary decision diagrams (BDDs) to analyse specified properties in BFL, patterns and an algorithm to construct counterexamples. Finally, we propose a case-study application of BFL by analysing a COVID-19related FT.
Original languageEnglish
Title of host publication2022 52nd Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN)
PublisherIEEE/EUCA
Pages441-452
Number of pages12
ISBN (Electronic)978-1-6654-1693-1
ISBN (Print)978-1-6654-1694-8
DOIs
Publication statusPublished - 30 Jun 2022
Event52nd Annual IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2022 - Baltimore, United States
Duration: 27 Jun 202230 Jun 2022
Conference number: 52

Conference

Conference52nd Annual IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2022
Abbreviated titleDSN 2022
Country/TerritoryUnited States
CityBaltimore
Period27/06/2230/06/22

Keywords

  • Industries
  • COVID-19
  • Systematics
  • Binary decision diagrams
  • Model checking
  • Software
  • Software reliability
  • Fault Trees
  • 22/3 OA procedure

Fingerprint

Dive into the research topics of 'BFL: a Logic to Reason about Fault Trees'. Together they form a unique fingerprint.

Cite this