Causality Checking

September 10, 2012
Stefan Leue | University of Konstanz

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.

Speaker Details

Stefan Leue is a Professor of Computer Science in the Department of Computer and Information Science at the University of Konstanz (Germany), where he holds the Chair for Software Engineering. His main research interests are in formal techniques for the design and analysis of complex systems. In particular, he is currently interested in variants of model checking, functional system safety analysis, system debugging, causality reasoning and the modeling and analysis of biological systems. He holds a PhD degree in Computer Science from the University of Berne (Switzerland), has held tenured faculty positions at the University of Waterloo (Canada) and the University of Freiburg (Germany) as well as visiting positions at Bell Laboratories (US), Université Joseph Fourier (France) and ETH Zurich (Switzerland). He is a member of the IEEE, the ACM and the GI.