Title
Efficient Anytime Techniques For Model-Based Safety Analysis
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.
Year
DOI
Venue
2015
10.1007/978-3-319-21690-4_41
COMPUTER AIDED VERIFICATION, PT I
Keywords
Field
DocType
Formal methods, Safety analysis, Fault tree, IC3, Parameter synthesis
Complex system,Computer science,Algorithm,Theoretical computer science,Formal methods,Certification,Fault tree analysis,Computation
Conference
Volume
ISSN
Citations 
9206
0302-9743
9
PageRank 
References 
Authors
0.56
17
4
Name
Order
Citations
PageRank
Marco Bozzano174349.82
Alessandro Cimatti25064323.15
Alberto Griggio362436.37
Cristian Mattarei4556.07