Formal analysis of fault tree using probabilistic model checking: A solar array case study

Fault Tree Analysis (FTA) is a widespread technique used to assess the reliability of safety-critical systems. The traditional way of conducting FTA is either through paper and pencil proof or through computer simulation techniques, which are inefficient and prone to inaccuracy. In this paper, we propose the use of probabilistic model checking to automatically analyze fault trees of safety-critical systems. Our methodology consists in the probabilistic formalization of the gates used in a fault tree to a Discrete-Time Markov Chain (DTMC) and a Markov Decision Process (MDP), and the subsequent probabilistic verification using PRISM tool to quantitatively analyze the system. To illustrate the proposed approach we perform the fault tree analysis of a solar array system, used as power source for the DFH-3 satellite. The results show that harsh thermal environment is the main cause of system failures.