Directed Model Checking

This project is joint work with Dr. Stefan Edelkamp and Alberto Lluch Lafuente of the Algorithms and Data Structures research group.

We investigate the use of directed search algorithms in explicit state model checking. The use of directed search algorithms decreases the number of expanded states when searching for safety property violations or when searching for acceptance cycles in liveness property analysis. At the same time, the error trails generated by the model checker are shorter and hence more comprehensible. So far we have applied this idea to Promela, which is the input language of the SPIN model checker. We validated safety properties (assertions, deadlock detection, invariants) and general temporal properties specified in LTL using the experimental HSF-SPIN workbench using a variety of communication protocols, including real-world protocols like the CORBA GIOP protocol.