Formal Analysis of Repairable Phased-Mission Systems with Common Cause Failures

Although several studies have been devoted to the reliability analysis of phased-mission systems (PMSs) considering the influence of common cause failures (CCFs), statistical correlation and repairable behavior still pose challenges to the analysis. In this article, a hierarchical formal model is proposed for the reliability analysis of repairable PMSs with CCFs. The low-level model is based on continuous time Markov chains and multiple beta factor theory used to construct the failure and repair behaviors of different missions under the effect of CCFs. The upper-level model realizes phase transition based on the Erlang distribution. The model can be implemented in PRISM, a tool that supports probabilistic model checking technology, and can be automatically verified by the properties (termed as reliability and availability in this article) defined by continuous stochastic logic. The proposed model introduces the benefits of probabilistic model checking into the analysis of PMSs for the first time. The formal hierarchical model is demonstrated by an example of a field programmable gate array system based on different design modes. Then, the influence of CCFs on the reliability of three different mission phase combinations are discussed. Our model can help researchers verify system properties for dynamic, complex, and continuous tasks in the initial design phase, thereby optimizing the design pattern or task arrangement.