Directed Model Checking
This project is joint work with Dr. Stefan Edelkamp and Dr. Alberto Lluch-Lafuente.
We investigate the use of directed, heuristics guided 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 easily 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.
Publications
-
Alberto Lluch-Lafuente, Stefan Edelkamp, Stefan Leue: Partial Order Reduction in Directed Model Checking,
Volume 2318, Proceedings of the 9th International SPIN Workshop on Software Model Checking, Lecture Notes in Computer Science,
Springer Verlag, 2002.
Abstract: 
Partial order reduction is a very succesful technique for avoiding the state explosion problem that is inherent to explicit state model checking of asynchronous concurrent systems. It exploits the commutativity of concurrently executed transitions in interleaved system runs in order to reduce the size of the explored state space. Directed model checking on the other hand addresses the state explosion problem by using guided search techniques during state space exploration. As a consequence, shorter errors trails are found and less search effort is required than when using standard depth-first or breadth-first search. We analyze how to combine directed modelchecking with partial order reduction methods and give experimental results on how the combination of both techniques performs.
Download: [PDF] [PS] -
Stefan Edelkamp, Stefan Leue, Alberto Lluch-Lafuente: Directed Explicit-State Model Checking in the Validation of Communication Protocols,
Technical Report No. 161, Institute for Computer Science, Albert-Ludwigs-University Freiburg, 2001.
Abstract: The success of model checking is largely based on its ability to efficiently locate errors in software designs. If an error is found, a model checker produces a trail that shows how the error state can be reached, which greatly facilitates debugging. However, while current model checkers find error states efficiently, the counterexamples are often unnecessarily lengthy, which hampers error explanation. This is due to the use of "naive" search algorithms in the state space exploration. In this paper we present approaches to the use of heuristic search algorithms in explicit-state model checking. We present the class of A* directed search algorithms and propose heuristics together with bitstate compression techniques for the search of safety property violations. We achieve great reductions in the length of the error trails, and in some instances render problems analyzable by exploring a much smaller number of states than standard depth-first search. We then suggest an improvement of the nested depth-first search algorithm and show how it can be used together with A* to improve the search for liveness property violations. Our approach to directed explicit-state model checking has been implemented in a tool set called HSF-SPIN. We provide experimental results from the protocol validation domain using HSF-SPIN.
Download: [PDF] [PS] -
Stefan Edelkamp, Alberto Luch Lafuente and Stefan Leue: Trail-Directed Model Checking, Proceedings of the Workshop on Software Model Checking,
Electrical Notes in Theoretical Computer Science, Elsevier, 2001.
Abstract: HSF-SPIN is a Promela model checker based on heuristic search strategies. It utilizes heuristic estimates in order to direct the search for finding software bugs in concurrent systems. As a consequence, HSF-SPIN is able to find shorter trails than blind depth-first search. This paper contributes an extension to the paradigm of directed model checking to shorten already established unacceptable long error trails. This approach has been implemented in HSF-SPIN. For selected benchmark and industrial communication protocols experimental evidence is given that trail-directed model-checking effectively shortcuts existing witness paths. -
Stefan Edelkamp, Alberto Lluch Lafuente, Stefan Leue: Directed Explicit Model Checking with HSF-SPIN, Proceedings 8th International SPIN Workshop
on Model Checking Software, Lecture Notes in Computer Science, Springer LNCS, Toronto, 2001.
Abstract: We present the explicit state model checker HSF-SPIN which is based on the model checker SPIN and its Promela modeling language. HSF-SPIN incorporates directed search algorithms for checking safety and a large class of LTL-specified liveness properties. We start off from the A* algorithm and define heuristics to accelerate the search into the direction of a specified failure situation. Next we propose an improved depth-first search algorithm that exploits the structure of Promela Never-Claims. As a result of both improvements, counterexamples will be shorter and the explored part of the state space will be smaller than with classical approaches, allowing to analyze larger state spaces. We evaluate the impact of the new heuristics and algorithms on a set of protocol models, some of which are real-world industrial protocols.
Download: [PDF] [PS] -
Stefan Edelkamp, Alberto Lluch Lafuente and Stefan Leue: Protocol Verification with Heuristic Search, Proceedings of the AAAI-ss01 Workshop
on Model-based Validation of Intelligence, Stanford University, 2001.
Abstract: We present an approach to reconcile explicit state model checking and heuristic directed search. We provide experimental evidence that the model checking problem for concurrent systems, such as communications protocols, can be solved more efficiently, since finding a state violating a property can be understood as a directed search problem. In our work we combine the expressive power and implementation efficiency of the SPIN model checker with the HSF heuristic search workbench, yielding the HSF-SPIN tool that we have implemented. We start off from the A* algorithm and some of its derivatives and define heuristics for various system properties that guide the search so that it finds error states faster. In this paper we focus on safety properties and provide heuristics for invariant and assertion violation and deadlock detection. We provide experimental results for applying HSF-SPIN to two toy protocols and one real world protocol, the CORBA GIOP protocol.
Download: [PDF] [PS]