Symbolic Fault Tree Analysis for Reactive Systems

14 years 1 months ago
Symbolic Fault Tree Analysis for Reactive Systems
Fault tree analysis is a traditional and well-established technique for analyzing system design and robustness. Its purpose is to identify sets of basic events, called cut sets, which can cause a given top level event, e.g. a system malfunction, to occur. Generating fault trees is particularly critical in the case of reactive systems, as hazards can be the result of complex interactions involving the dynamics of the system and of the faults. Recently, there has been a growing interest in model-based fault tree analysis using formal methods, and in particular symbolic model checking techniques. In this paper we present a broad range of algorithmic strategies for efficient fault tree analysis, based on binary decision diagrams (BDDs). We describe different algorithms encompassing different directions (forward or backward) for reachability analysis, using dynamic cone of influence techniques to optimize the use of the finite state machine of the system, and dynamically pruning of the f...
Marco Bozzano, Alessandro Cimatti, Francesco Tappa
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Where ATVA
Authors Marco Bozzano, Alessandro Cimatti, Francesco Tapparo
Comments (0)