Statusvortrag im Rahmen des Promotionsver­fahrens von Herrn Johannes Lehmann

Abstract:

Model checking is a widely used technique to ensure the formal correctness of systems. However, the output of model checking tools is often insufficient for explaining why a system violates a specification.

To address this deficiency, this talk introduces the notion of backward responsibility: Given a specific failure of a system, we ascribe a responsibility value to each system state based on whether the state could have prevented the failure. We use the Shapley value, a well-known concept from game theory, to transform the qualitative data (“In which contexts can the state prevent the failure?”) into a quantitative responsibility value.

 After providing the basic construction, we extend the results from individual states to groups of states and show how suitable state groups can be extracted automatically from high-level model specifications. Finally, we discuss the computational complexity of the responsibility value, present algorithms that handle specific instances of the problem efficiently and evaluate them using a prototypical implementation.