Abstract
I will introduce Causality Checking, a technique extending model checking designed to establish causalities for safety property violations in system models. Causality Checking is based on counterfactual reasoning. In particular, it is based on an adoption of the Halpern/Pearl Structural Equation Model (SEM) for establishing actual causes. Causality Checking takes advantage of the fact that using a model checker it is fairly easy to compute both "bad" as well as alternate "good" worlds, where a world corresponds to a finite execution sequence.

Based on our adoption of the SEM I will show how causalities can be determined by performing difference computations on the sets of bad and good executions of a model. I will present two approaches how to perform this computation: one based on an explicit enumeration of all bad and good execution traces of a model, and another one based on an on-the-fly algorithm integrated into standard state space search algorithms used in explicit state model checking. I will sketch applications of Causality Checking to systems analysis by considering a number of case studies, including functional and probabilistic models. I will illustrate how the computed causalities can be displayed as fault trees and serve as a basis for system debugging.

This is joint work with Florian Leitner-Fischer.