University of Konstanz
Graduiertenkolleg / PhD Program
Computer and Information Science

Guest Talks

title

Towards an Integrated Counterexample-guided Abstraction Refinement for Real-Time Systems

speaker

Prof. Dr. Henning Dierks, University of Oldenburg
Oldenburg, Germany

date & place

Thursday, 19.11.2009, 10:00 h
Room R 512

abstract

In this talk we will present our results in the area of automatic verification of real-time systems. Our aim is to achieve an integrated counterexample guided abstraction refinement loop for such systems. Provided that a model-checking tool is given there are some prerequisites to implement such an approach efficiently:
  1. Hierarchically structured abstractions for the formalism to be checked.
  2. A technique to reduce the time for model-checking coarse abstractions.
  3. A technique to refine abstractions appropriately in case of spurious counterexamples. This is needed to deal with the situation in which an abstract counterexample is found but there is no counterpart in the full model. In this case the current abstraction was too coarse and it must be refined.
For (2) we will demonstrate that directed model-checking can be applied successfully because this technology improves the falsification of safety properties by providing heuristic functions that can guide the search quickly towards short error paths.
For (3) we will show how to use the generated abstract counterexample to construct either a concrete counterexample for the full model or to identify a slightly refined abstraction in which the found spurious counterexample cannot occur anymore.