University of Konstanz
Graduiertenkolleg / PhD Program
Computer and Information Science

Graduation Talks


Directed diagnostics of system dependability models


Husain Aljazzar, University Konstanz
Konstanz, Germany

date & place

Wednesday, 04.07.2007, 16:00 h
Room C252


Correctness, dependability and performance are major quality aspects of computer systems. A variety of methods and tools have been developed and used to improve these quality aspects. One of these methods is model checking. Its success can be attributed to the fact that it performs an automated analysis, and that model checkers return offending paths from the initial state to the error state, i.e., a state which violates a desired system property, if such a state is reachable. Such a counterexample, as those offending paths are commonly called, is a proof for the property violation. It is also essential for debugging, i.e., localising and fixing the fault which caused that property violation.

To obtain short and therefore easy to comprehend counterexamples, search techniques such as Breadth- First Search (BFS) or Directed Model Checking (DMC) can be employed. DMC relies on heuristics-guided, also called directed, search algorithms, e.g. A* and Z*. These algorithms are based on the general-purpose strategy Best-First (BF) which has been introduced to solve problems of, amongst others, graph search and optimization.