Safety analysis investigates system behavior under faulty conditions. It is a fundamental step in the design of complex systems, that is often mandated by certification procedures. Safety analysis includes two key steps: the construction of all minimal cut sets (MCSs) for a given property (i.e. the sets of basic faults that may cause a failure), and the computation of the corresponding probability (given probabilities for the basic faults). Model-based Safety Analysis relies on formal verification to carry out these tasks. However, the available techniques suffer from scalability problems, and are unable to provide useful results if the computation does not complete. In this paper, we investigate and evaluate a family of IC3-based algorithms for MCSs computation. We work under the monotonicity assumption of safety analysis (i.e. an additional fault can not prevent the violation of the property). We specialize IC3-based routines for parameter synthesis by optimizing the counterexample generalization, by ordering the exploration of MCSs based on increasing cardinality, and by exploiting the inductive invariants built by IC3 to accelerate convergence. Other enhancements yield an “anytime” algorithm, able to produce an increasingly precise probability estimate as the discovery of MCSs proceeds, even when the computation does not terminate. A thorough experimental evaluation clearly demonstrates the substantial advances resulting from the proposed methods.

Efficient Anytime Techniques for Model-Based Safety Analysis / Bozzano, Marco; Cimatti, Alessandro; Griggio, Alberto; Mattarei, Cristian. - STAMPA. - 9206:(2015), pp. 603-621. (Intervento presentato al convegno 27th International Conference on Computer Aided Verification, CAV 2015 tenutosi a San Francisco, CA nel July 18-24, 2015) [10.1007/978-3-319-21690-4_41].

Efficient Anytime Techniques for Model-Based Safety Analysis

Cimatti Alessandro;Griggio Alberto;Mattarei Cristian
2015-01-01

Abstract

Safety analysis investigates system behavior under faulty conditions. It is a fundamental step in the design of complex systems, that is often mandated by certification procedures. Safety analysis includes two key steps: the construction of all minimal cut sets (MCSs) for a given property (i.e. the sets of basic faults that may cause a failure), and the computation of the corresponding probability (given probabilities for the basic faults). Model-based Safety Analysis relies on formal verification to carry out these tasks. However, the available techniques suffer from scalability problems, and are unable to provide useful results if the computation does not complete. In this paper, we investigate and evaluate a family of IC3-based algorithms for MCSs computation. We work under the monotonicity assumption of safety analysis (i.e. an additional fault can not prevent the violation of the property). We specialize IC3-based routines for parameter synthesis by optimizing the counterexample generalization, by ordering the exploration of MCSs based on increasing cardinality, and by exploiting the inductive invariants built by IC3 to accelerate convergence. Other enhancements yield an “anytime” algorithm, able to produce an increasingly precise probability estimate as the discovery of MCSs proceeds, even when the computation does not terminate. A thorough experimental evaluation clearly demonstrates the substantial advances resulting from the proposed methods.
2015
Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I
Cham, Switzerland
Springer
Bozzano, Marco; Cimatti, Alessandro; Griggio, Alberto; Mattarei, Cristian
Efficient Anytime Techniques for Model-Based Safety Analysis / Bozzano, Marco; Cimatti, Alessandro; Griggio, Alberto; Mattarei, Cristian. - STAMPA. - 9206:(2015), pp. 603-621. (Intervento presentato al convegno 27th International Conference on Computer Aided Verification, CAV 2015 tenutosi a San Francisco, CA nel July 18-24, 2015) [10.1007/978-3-319-21690-4_41].
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: https://hdl.handle.net/11572/343003
 Attenzione

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

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 22
  • ???jsp.display-item.citation.isi??? 14
social impact