Explaining Counterexamples Using Causality

10 years 2 months ago
Explaining Counterexamples Using Causality
Abstract. When a model does not satisfy a given specification, a counterexample is produced by the model checker to demonstrate the failure. A user must then examine the counterexample trace, in order to visually identify the failure that it demonstrates. If the trace is long, or the specification is complex, finding the failure in the trace becomes a non-trivial task. In this paper, we address the problem of analyzing a counterexample trace and highlighting the failure that it demonstrates. Using the notion of causality, introduced by Halpern and Pearl, we formally define a set of causes for the failure of the specification on the given counterexample trace. These causes are marked as red dots and presented to the user as a visual explanation of the failure. We study the complexity of computing the exact set of causes, and provide a polynomial-time algorithm that approximates it. This algorithm is implemented as a feature in the IBM formal verification platform RuleBase PE, where thes...
Ilan Beer, Shoham Ben-David, Hana Chockler, Avigai
Added 25 Nov 2009
Updated 25 Nov 2009
Type Conference
Year 2009
Where CAV
Authors Ilan Beer, Shoham Ben-David, Hana Chockler, Avigail Orni, Richard J. Trefler
Comments (0)