Debugging of Dependability Models Using Interactive Visualization of Counterexamples

The authors present an approach to support the debugging of stochastic system models using interactive visualization. The goal of this paper is to facilitate the identification of causal factors in the potentially very large sets of execution traces that form counterexamples in stochastic model checking. The visualization is interactive and allows the user to focus on the most meaningful aspects of a counterexample. They present the application of the visualization method as implemented in their prototype tool DIPRO to two significant case studies.