Solving Queries for Boolean Fault Tree Logic via Quantified SAT
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.
Sun 22 OctDisplayed time zone: Lisbon change
11:00 - 12:30 | Paper presentationsFTSCS at Room IV Chair(s): Cyrille Artho KTH Royal Institute of Technology, Sweden | ||
11:00 30mTalk | Probabilistic Risk Assessment of an Obstacle Detection System for GoA 4 Freight Trains FTSCS | ||
11:30 30mTalk | Solving Queries for Boolean Fault Tree Logic via Quantified SAT FTSCS Caz Saaltink , Stefano M. Nicoletti , Matthias Volk , Ernst Moritz Hahn Queen's University Belfast, Marielle Stoelinga University of Twente and Radboud University, Nijmegen | ||
12:00 30mTalk | Symbolic analysis by using folding narrowing with irreducibility and SMT constraints FTSCS |