Franz Weitl

Current Project: CITE - From Counterexamples to Interactive Incremental Tracing of Errors

CITE aims at developing the fundamental methods for generating both comprehensive and comprehensible error reports based on model checking results.
Model checking is a powerful and efficient method for finding flaws in hardware designs, object-oriented software, business processes, and hypermedia applications. One remaining major obstacle to a broader application of model checking is its limited usability for non-experts. It requires much effort and insight to determine the root cause of errors from counterexamples generated by model checkers in the case of a specification violation. The CITE project addresses this problem in two ways: First, a new interactive and incremental process of generating counterexamples is proposed which supports focused successive refinement of verification results at the user’s demand, thus avoiding information overflow caused by bulky counterexamples. Second, a relational representation layer, based on temporal description logics, enables error tracing along semantic relationships of objects. First results indicate that the combination of these methods provides unmatched user support in error tracking while maintaining full compatibility with existing model checking tools and applications.

For further information and publications related to the CITE project, check the Verdikt project at the University of Passau: www.verdikt.uni-passau.de