Causality Checking and the QuantUM Tool
Stefan Leue
University of Konstanz, Germany
http://se.uni-konstanz.de
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 based on bounded model checking and SAT solving.
Computing causalities is particularly relevant in the safety analysis of safety-critical embedded systems, for instance when performing fault tree analysis. We have developed a model-based approach to functional safety that takes SysML models from industrial design tools, such as Rational Rhapsody, and performs an automated fault tree analysis based on causality checking on them. I will introduce the related QuantUM approach and tool and present a number of industrial case studies.
Biography of the speaker:
Prof. Leue has been a Full Professor of Computer Science and holder of the Chair for Software and Systems Engineering at the University of Konstanz since 2004. His research interests are in methods supporting the design and analysis of complex systems, with special interest in cyber-physical and biological systems. Prior academic appointments include faculty positions at the University of Freiburg (Germany, 2000-2004) and at the University of Waterloo (Canada, 1995-2001) as well as a member of techical staff appointment at Bell Laboratories (USA, 1998). He holds a PhD in computer science from the University of Berne (Switerland) and is a member of the ACM, IEEE and the GI.
