Solving Queries for Boolean Fault Tree Logic via Quantified SAT

Caz Saaltink, Stefano M. Nicoletti*, Matthias Volk, Ernst Moritz Hahn, Mariëlle Stoelinga

*Corresponding author for this work

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

4 Downloads (Pure)

Abstract

Fault trees (FTs) are hierarchical diagrams used to model the propagation of faults in a system. Fault tree analysis (FTA) is a widespread technique that allows to identify the key factors that contribute to system failure. In recent work we introduced BFL, a Boolean Logic for Fault trees. BFL can be used to formally define simple yet expressive properties for FTA, e.g.: 1) we can set evidence to analyse what-if scenarios; 2) check whether two elements are independent or if they share a child that can influence their status; 3) and set upper/lower boundaries for failed elements. Furthermore, we provided algorithms based on binary decision diagrams (BDDs) to check BFL properties on FTs. In this work, we evaluate usability of a different approach by employing quantified Boolean formulae (QBFs) instead of BDDs. We present a translation from BFL to QBF and provide an implementation—making it the first tool for checking BFL properties—that builds on top of the Z3 solver. We further demonstrate its usability on a case study FT and investigate runtime, memory consumption and scalability on a number of benchmark FTs. Lastly, qualitative differences from a BDD-based approach are discussed.
Original languageEnglish
Title of host publicationFTSCS 2023: Proceedings of the 9th ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems
Subtitle of host publication2023 Proceeding
EditorsCyrille Artho, Peter Csaba Olveczky
PublisherACM Press
Pages48-59
Number of pages12
ISBN (Electronic)9798400703980
ISBN (Print)979-8-4007-0398-0
DOIs
Publication statusPublished - 19 Oct 2023
EventNinth ACM International Workshop on Formal Techniques for Safety-Critical System (FTSCS 2023) - Cascais, Portugal
Duration: 22 Oct 202322 Oct 2023
Conference number: 9
https://2023.splashcon.org/home/ftscs-2023

Conference

ConferenceNinth ACM International Workshop on Formal Techniques for Safety-Critical System (FTSCS 2023)
Abbreviated titleFTSCS 2023
Country/TerritoryPortugal
CityCascais
Period22/10/2322/10/23
Internet address

Keywords

  • 2023 OA procedure

Fingerprint

Dive into the research topics of 'Solving Queries for Boolean Fault Tree Logic via Quantified SAT'. Together they form a unique fingerprint.

Cite this