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
Topic
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.