Model Checking has proven to be an effective software verification
technique. Explicit-state model checking, as for instance implemented
in the popular tool SPIN, has proven particularly successful in
the analysis of concurrent software systems. The popularity of
explicit-state model checkers is due to, amongst others, the fact that
when a property violation is found, the model checker returns a trail
leading from the initial system state into the property violating
state. This greatly helps fault explanation. Most explicit-state model
checkers perform depth-first searches on the state space. While this
is memory efficient, the resulting error trails can be very long.
We discuss alternatives to the state space explorations that address
this problem. These include breadth-first searches, iterated deepening
searches, and, most importantly, heuristic guide searches such as A*
and iterative deepening A*. We will show how heuristic functions can
be determined and illustrate applications of directed explicit-state
model checking to the validation of safety and liveness properties. We
finally prove that directed explicit-state model checking can be used
effectively even in the presence of partial-order reduction.
______________________________________________________________________
Das Logikseminar ist eine gemeinsame Veranstaltung des DFKI, des MPI
und der Fachrichtungen Informatik, Philosophie und Rechtswissenschaft.
Vortragswünsche bitte an Uwe Waldmann, MPI, Tel.: (0681) 9325-227,
uni-intern: 92227, E-Mail: #email not disclosed#