[Chair]  [Computer Science Department (FBI)]  [University Dortmund] 



Spezialvorlesung Sommersemester 2007
Gerichtete Modellprüfung
(Directed Model Checking)

Veranstalter: PD Dr. Stefan Edelkamp
Termin: Mi. 10:15-12:00, Raum: Otto-Hahn-Str. 14, R 104


Heuristic guided search techniques have first been proposed in the area of AI where they have been used quite successfully in solving complex planning and scheduling problems. On the other hand, Model Checking has evolved into one of the most successful verification techniques. Examples range from mainstream applications such as protocol validation, software model checking and embedded systems verification to exotic areas such as business workflow analysis, scheduler synthesis and planning. Model checking technology has also been proven to be effective in automated test case generation.

The sheer size of the reachable state space of realistic models imposes tremendous challenges on the algorithmics of model checking technology. Complete exploration of the state space is often unfeasible and approximations are needed. Also, the error trails reported by depth-first search model checkers are often exceedingly lengthy -- in many cases they consist of mutliple thousands of computation steps which greatly hampers error interpretation. In the meantime, state space exploration is a central aspect of AI, and the AI community has a long and impressive line of research in developing and improving search algorithms over very large state spaces under a broad range of assumptions.

The term "Directed Model Checking" was coined by an paper on the application of heuristic search in the symbolic model checker checker mucke. Earlier work mainly included best-first search-like search strategies for accelerating the search for concrete type of errors in the model cheker Murphi. Since then the interest on applying AI-based search techniques grew and was applied in different domains: Java and C++ programs, real-time systems, hardware circuits. In some cases ressearch produced or extended verification tools with heuristic search capabilities. We mention, among others, HSF-SPIN (an extension of the SPIN model checker), Java Path Finder and UPPAAL. There are also some first attempts in applying heuristic search to improve proof-state based theorem provers such as Isabelle.

Usually one distinguishes various aspects in the verification of systems. First, due to the complexity of concurrent and distributed systems, errors are very likely to appear and one desires to find them as quickly as possible. Next, one looks for short error trails, easier to understand than longer ones. Since the requirements of the these two phases are not the same, different heuristic search strategies apply.

Content Highlights

Directed Explicit-State Model Checking: In this context, we study directed search in explicit state LTL model checking. We address the combination of heuristic search with bit-state hashing, iterative deepening, symmetry reduction, partial-order reduction, external search, genetic algorithms and automated abstractions in form of databases, just to name a few.

Directed Symbolic Model Checking: We extend previous approaches to "symbolic model checking" by devising a BDD version of the A* algorithm. e.g. for the mucke model checker. Our main focus is the exploration with abstractions.

Directed CTL* Model Checking: We show how to extend the AO* algorithm is the adequate extension to perform combined LTL and CTL model checking. The heurstics are derived in form of abstractions.

Directed Model Checking Integrated Planning: With a compilation scheme of MC inputs into planning specifications, we study the possibility of using planners to perform model checking directly. Simple protocols have been successfully tested as benchmarks in international planning competitions. We extend the applicability to larger protocol designs.

Directed Bytecode Model Checking: The "Java Pathfinder" project is probably the leading tool to explore software programs without referring to an abstract model. It uses a model checker on top of a virtual machine. Much of the efficiency has been gained by using structural heuristics in form of source code metrics.

Directed Assembly Model Checking: The directed program model checker StEAM extends the design principle of the Pathfinder to object code verification. The bypasses modelling and operates on any binary that has been compiled from c/c++. A virtual machine for executing ELF binaries has been found and extended to model check such "assemblies". We study state reconstruction schemes and incremental hash functions.

Directed Model Checking

Stefan Edelkamp (stefan.edelkamp@cs.uni-dortmund.de)