BFL: a Logic to Reason about Fault Trees

TL;DR

This paper introduces Boolean Fault Tree Logic (BFL), a new formal logic framework with model checking algorithms for analyzing fault trees, enhancing the ability to formulate and verify complex safety scenarios in critical systems.

Contribution

The paper presents BFL, a novel logic for fault tree analysis, along with model checking algorithms and a case study demonstrating its practical application.

Findings

BFL enables more expressive fault tree analysis queries.

Model checking with BDDs efficiently verifies fault tree properties.

Case study shows BFL's effectiveness in analyzing COVID-19 fault scenarios.

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 COVID19-related FT.