Efficient probabilistic fault tree analysis of safety critical systems via probabilistic model checking

The cost and complexity involved in the development of critical systems encourage the use of reliability assessment techniques as early in the design cycle as possible. Existing techniques often lack the capacity to perform a comprehensive and exhaustive analysis on complex redundant architectures, leading to less than optimal risk evaluation. This paper addresses these weaknesses by 1) proposing a new probabilistic modeling of Fault Tree gates and their composition as Markov Decision Processes; 2) developing a new formal-based technique to perform an in-depth verification of the system's reliability. This technique makes use of the expressiveness of fault trees and the power of probabilistic model checking in order to investigate the best Triple Modular Redundancy partitioning and configuration of a system. The presented approach greatly improves the overall scalability with respect to other techniques, while also improving the accuracy of the results. For example, we can provide probabilistic failure rates for a chain of 100 redundant components in little over one second.