Towards Formal Fault Tree Analysis Using Theorem Proving
From MaRDI portal
Publication:3453105
DOI10.1007/978-3-319-20615-8_3zbMATH Open1417.68174arXiv1505.02648OpenAlexW2963684489MaRDI QIDQ3453105FDOQ3453105
Authors: Waqar Ahmed, Osman Hasan 
Publication date: 20 November 2015
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Abstract: Fault Tree Analysis (FTA) is a dependability analysis technique that has been widely used to predict reliability, availability and safety of many complex engineering systems. Traditionally, these FTA-based analyses are done using paper-and-pencil proof methods or computer simulations, which cannot ascertain absolute correctness due to their inherent limitations. As a complementary approach, we propose to use the higher-order-logic theorem prover HOL4 to conduct the FTA-based analysis of safety-critical systems where accuracy of failure analysis is a dire need. In particular, the paper presents a higher-order-logic formalization of generic Fault Tree gates, i.e., AND, OR, NAND, NOR, XOR and NOT and the formal verification of their failure probability expressions. Moreover, we have formally verified the generic probabilistic inclusion-exclusion principle, which is one of the foremost requirements for conducting the FTA-based failure analysis of any given system. For illustration purposes, we conduct the FTA-based failure analysis of a solar array that is used as the main source of power for the Dong Fang Hong-3 (DFH-3) satellite.
Full work available at URL: https://arxiv.org/abs/1505.02648
Recommendations
- Formal fault tree analysis -- practical experiences
- Probabilistic analysis of dynamic fault trees using HOL theorem proving
- Formalization of fault trees in higher-order logic: a deep embedding approach
- Formal Reliability Analysis Using Theorem Proving
- A verified realization of a Dempster-Shafer based fault tree analysis
- Formalization of fault analysis and a new approach of fault detection
- Fault tree analysis: a survey of the state-of-the-art in modeling, analysis and tools
- Formally verifying fault tolerant system designs
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Toward a theory of fuzzy information granulation and its centrality in human reasoning and fuzzy logic
- Title not available (Why is that?)
- Three chapters of measure theory in Isabelle/HOL
- Towards the formal reliability analysis of oil and gas pipelines
- On the formalization of the Lebesgue integration theory in HOL
- Formalization of Continuous Probability Distributions
- An approach for lifetime reliability analysis using theorem proving
- Title not available (Why is that?)
- Title not available (Why is that?)
- Formal fault tree analysis -- practical experiences
Cited In (16)
- FM 2005: Formal Methods
- A framework for formal dynamic dependability analysis using HOL theorem proving
- Formalization of functional block diagrams using HOL theorem proving
- Dynamic dependability analysis of shuffle-exchange networks
- Failure propagation modeling and analysis via system interfaces
- Formal reliability analysis of combinational circuits using theorem proving
- Formal dependability modeling and analysis: a survey
- Formalization of RBD-based cause consequence analysis in HOL
- Formalization of reliability block diagrams in higher-order logic
- Formal Verification of Rewriting Rules for Dynamic Fault Trees
- A framework for formal probabilistic risk assessment using \textsf{HOL} theorem proving
- Formal reliability and failure analysis of Ethernet based communication networks in a smart grid substation
- Probabilistic analysis of dynamic fault trees using HOL theorem proving
- Towards the formal reliability analysis of oil and gas pipelines
- Formalization of fault trees in higher-order logic: a deep embedding approach
- Formal fault tree analysis -- practical experiences
Uses Software
This page was built for publication: Towards Formal Fault Tree Analysis Using Theorem Proving
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3453105)
