Probabilistic analysis of dynamic fault trees using HOL theorem proving

被引：0

作者：

Elderhalli, Yassmeen ^{[1
]}

Ahmad, Waqar ^{[1
]}

Hasan, Osman ^{[1
]}

Tahar, Sofiène ^{[1
]}

机构：

[1] Electrical and Computer Engineering, Concordia University, Montreal,QC, Canada

来源：

Journal of Applied Logics | 2019年 / 6卷 / 03期

关键词：

Forestry - Failure (mechanical) - Theorem proving;

D O I：

暂无

中图分类号：

学科分类号：

摘要：

Dynamic Fault Trees (DFTs) is a widely used failure modeling technique that allows capturing the dynamic failure characteristics of systems in a very effective manner. Simulation and model checking have been traditionally used for the probabilistic analysis of DFTs. Simulation is usually based on sampling and thus its results are not guaranteed to be complete, whereas model checking employs computer arithmetic and numerical algorithms to compute the exact values of probabilities, which contain many round-off errors. Leveraging upon the expressive and sound nature of higher-order-logic (HOL) theorem proving, we propose, in this paper, a formalization of DFT gates and their probabilistic behaviors as well as some of their simplification properties in HOL based on the algebraic approach. This formalization would allow us to conduct the probabilistic analysis of DFTs by verifying generic mathematical expressions about their behavior in HOL. In particular, we formalize the AND, OR, Priority-AND, Functional DEPendency, Hot SPare, Cold SPare and the Warm SPare gates and also verify their corresponding probabilistic expressions in HOL. Moreover, we formally verify an important property, P r(X © 2019, College Publications. All rights reserved.

引用

页码：469 / 511