Symbolic Encoding of Reliability for the Design of Redundant Architectures

In this paper, we propose an approach to automatic optimization of redundant embedded system architectures. Given a high-level description of a system and a library of redundant design patterns, all valid redundant alternative architectures are considered. Then, a model of the deviation of the architecture from its nominal behavior is built, and the set of all fault configurations, also referred to as 'cut sets', is computed. This can be used to extract a reliability function for the architecture under study. We leverage the power of Satisfiability Modulo Theory to encode the problem with a symbolic technique, and use the reliability function, together with the assessment of other design objectives, to compare different redundant configurations, thus supporting the exploration of the design space.