Formal reliability analysis of redundancy architectures

Reliability is a fundamental property for critical systems. A thorough evaluation of the reliability is required by the certification procedures in various application domains, and it is important to support the exploration of the space of the design solutions. In this paper we propose a new, fully automated approach to the reliability analysis of complex redundant architectures. Given an abstract description of the architecture, the approach automatically extracts a fault tree and a symbolic reliability function, i.e. a program mapping the probability of fault of the basic components to the probability that the overall architecture deviates from the expected behavior. The proposed approach heavily relies on formal methods, by representing the architecture blocks as Uninterpreted Functions, and using the so-called miter construction to model the deviation from the nominal behavior. The extraction of all the deviation conditions is reduced to an AllSMT problem, and we extract the reliability function by traversing the Binary Decision Diagram corresponding to the quantified formula. Predicate abstraction is used to partition and speed up the computation. The approach has been implemented leveraging formal tools for model checking and safety assessment. A thorough experimental evaluation demonstrates its generality and effectiveness of the proposed techniques.