  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.
