Automated Analysis of Reliability Architectures

The development of complex and critical systems calls for a rigorous and thorough the evaluation of reliability aspects. Over the years, several methodologies have been introduced in order to aid the verification and analysis of such systems. Despite this fact, current technologies are still limited to specific architectures, without providing a generic evaluation of redundant system definitions. In this paper we present a novel approach able to assess the reliability of an arbitrary combinatorial redundant system. We rely on an expressive modeling language to represent a wide class of architectural solutions to be assessed. On such models, we provide a portfolio of automatic analysis techniques: we can produce a fault tree, that represents the conditions under which the system fails to produce a correct output; based on it, we can provide a function over the components reliability, which represents the failure probability of the system. At its core, the approach relies on the logical formalism of equality and uninterpreted functions; it relies on automated reasoning techniques, in particular Satisfiability Modulo Theories decision procedures, to achieve efficiency. We carried out an extensiver experimental evaluation of the proposed approach on a wide class of multi-stage redunded systems. On the one hand, we are able to automatically obtain all the results that are manually obtained in [1]; on the other, we provide results for a much wider class of architectures, including the cases of non-uniform probabilities and of two voters per stage.