Causality Checking

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 introduce an on-the-fly Causality Checking algorithm integrated into standard state space search algorithms used in explicit state model checking. I will then sketch applications of Causality Checking to systems analysis by considering a number of case studies, including functional and probabilistic models. Using these case studies I will compare Causality Checking to an off-line computation of causal relationships based on probabilistic models. I will finally illustrate how the computed causalities can be displayed as fault trees and serve as a basis for system debugging.