The overall safety of critical systems is often based on the use of redundant architectural patterns, such as Triple Modular Redundancy. Certification procedures in various application domains require an explicit evaluation of the reliability, and the production of various artifacts. Particularly interesting are Fault Trees (FT), that represent in a compact form all the combinations of (basic) faults that are required to cause a (system-level) failure. Yet, such activities are essentially based on manual analysis, and are thus time consuming and error prone. A recently proposed approach opens the way to the automated analysis of reliability architectures. The approach is based on the use of Satisfiability Modulo Theories (SMT), using the theory of Equality and Uninterpreted Functions (EUF) to represent block diagrams. Within this framework, the construction of FTs is based on the existential quantification of an EUF formula. Unfortunately, the off-the-shelf application of available techniques, based on the translation into an AllSMT problem, suffers from severe scalability issues. In this paper, we propose a compositional method to solve this problem, based on the use of predicate abstraction. We prove that our method is sound and complete for a wide class of system architectures. The presented approach greatly improves the overall scalability with respect to the monolithic case, obtaining speed-ups of various orders of magnitude. In practice, this approach allows for the verification of architectures of realistic systems.

Efficient Analysis of Reliability Architectures via Predicate Abstraction

Bozzano, Marco;Cimatti, Alessandro;Mattarei, Cristian
2013

Abstract

The overall safety of critical systems is often based on the use of redundant architectural patterns, such as Triple Modular Redundancy. Certification procedures in various application domains require an explicit evaluation of the reliability, and the production of various artifacts. Particularly interesting are Fault Trees (FT), that represent in a compact form all the combinations of (basic) faults that are required to cause a (system-level) failure. Yet, such activities are essentially based on manual analysis, and are thus time consuming and error prone. A recently proposed approach opens the way to the automated analysis of reliability architectures. The approach is based on the use of Satisfiability Modulo Theories (SMT), using the theory of Equality and Uninterpreted Functions (EUF) to represent block diagrams. Within this framework, the construction of FTs is based on the existential quantification of an EUF formula. Unfortunately, the off-the-shelf application of available techniques, based on the translation into an AllSMT problem, suffers from severe scalability issues. In this paper, we propose a compositional method to solve this problem, based on the use of predicate abstraction. We prove that our method is sound and complete for a wide class of system architectures. The presented approach greatly improves the overall scalability with respect to the monolithic case, obtaining speed-ups of various orders of magnitude. In practice, this approach allows for the verification of architectures of realistic systems.
978-3-319-03076-0
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11582/184210
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact