面向定理证明的形式化故障树分析

故障树分析 (FTA) 是一种可靠性分析技术，被广泛用于预测许多复杂工程系统的可靠性、可用性和安全性。传统上，这些基于 FTA 的分析是通过纸笔证明方法或计算机仿真完成的，由于其固有局限性而无法确保绝对正确性。作为一种补充方法，我们提议使用高阶逻辑定理证明器 HOL4 来对安全关键系统进行基于 FTA 的分析，此类系统极需故障分析的精确性。具体而言，本文给出了通用故障树门（即 AND、OR、NAND、NOR、XOR 和 NOT）的高阶逻辑形式化及其失效概率表达式的形式验证。此外，我们正式验证了通用概率容斥原理，它是进行任意给定系统基于 FTA 的失效分析的首要要求之一。为说明目的，我们对作为东方红三号 (DFH-3) 卫星主电源的光伏阵列进行了基于 FTA 的失效分析。