English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Dynamic Fault Trees (DFTs) is a widely used failure modeling technique thatallows capturing the dynamic failure characteristics of systems in a veryeffective manner. Simulation and model checking have been traditionally usedfor the probabilistic analysis of DFTs. Simulation is usually based on samplingand thus its results are not guaranteed to be complete, whereas model checkingemploys computer arithmetic and numerical algorithms to compute the exactvalues of probabilities, which contain many round-off errors. Leveraging uponthe expressive and sound nature of higher-order-logic (HOL) theorem proving, wepropose, in this work, a formalization of DFT gates and their probabilisticbehavior as well as some of their simplification properties in HOL. Thisformalization would allow us to conduct the probabilistic analysis of DFTs byverifying generic mathematical expressions about their behavior in HOL. Inparticular, we formalize the AND, OR, Priority-AND, Functional DEPendency, HotSPare, Cold SPare and the Warm SPare gates and also verify their correspondingprobabilistic expressions in HOL. Moreover, we formally verify an importantproperty, Pr(X<Y), using the Lebesgue integral as this relationship allows usto reason about the probabilistic properties of Priority-AND gate and theBefore operator. We also formalize the notion of conditional densities in orderto formally verify the probabilistic expressions of the Cold SPare and the WarmSPare gates. For illustrating the usefulness of our formalization, we use it toformally analyze the DFT of a Cardiac Assist System.

Formal Probabilistic Analysis of Dynamic Fault Trees in HOL4