Seminar: Directed Model Checking

Explicit-State Model Checking

Gerard J. Holzmann: The SPIN Model Checker -- Primer And Reference Manual,  Addison-Wesley, 2003, ISBN 0-321-22862-6, Chapter 8 (Search Algorithms)
Abstract:
In this chapter we will discuss the basic algorithms that SPIN uses to verify correctness properties of PROMELA models. The basic algorithms are fairly simple and can quickly be explained. But, if we are interested in applying a verifier to problems of practical size, the mere basics do not always suffice. There are many ways in which the memory use and the run-time requirements of the basic algorithms can be optimized. Perhaps SPIN's main strength lies in the range of options it offers to perform such optimizations, so that even very large problem sizes can be handled efficiently. To structure the discussion somewhat, we will discuss the main optimization methods that SPIN uses separately, in the next chapter. In thins chapter we restrict ourselves to a discussion of the essential elements of the search method that SPIN employs.
We start with the definition of a depth-first search algorithm, which we can then extend to perform the types of functions we need for systems verification.

Heuristic Search Algorithms

Judea Pearl: Heuristics -- Intelligent Search Strategies for Computer Problem Solving, Addision-Wesley, 1986, ISBN 0-201-05594-5, Chapter 2 (Basic Heuristic-Search Procedures)
Abstract:
In this chapter we describe the basic search strategies used in problem solving with special attention to the way in which they incorporate heuristic information. In chapter 1, we saw that many types of problems are conveniently described as tasks of finding some properties of graphs. Our current paradigm therefor is to find efficient methods of unraveling some properties of graphs using information from sources outside the graph.
Our discussion will be made easier by compiling some basic nomenclature regarding graphs and graph searching, although some of the concepts were ready used in Chapter 1.

Directed Explicit-State Model Checking

Stefan Edelkamp, Stefan Leue and Alberto Lluch-Lafuente: Directed Explicit-State Model Checking in the Validation of Communication Protocols, Software Tools for Technology Transfer (STTT), 2004, Volume 5 (2-3),  Pages 247-267, Springer Berlin / Heidelberg
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.

Keywords:  Model checking - Directed search - Protocol validation

Heuristics for Model Checking Java Programs

Alex Groce, Willem Visser: Heuristics for Model Checking Java Programs. Software Tools for Technology Transfer (STTT), 2004, Volume 6 (4), Pages 260-276, Springer Berlin / Heidelberg
Abstract:
Model checking of software programs has two goals -- the verification of correct software and the discovery of errors in faulty software. Some techniques for dealing with the most crucial problem in model checking, the state space explosion problem, concentrate on the first of these goals. In this paper we present an array of heuristic model checking techniques for combating the state space explosion when searching for errors. Previous work on this topic has mostly focused on property-specific heuristics closely related to particular kinds of errors. We present structural heuristics that attempt to explore the structure (branching structure, thread interdependency structure, abstraction structure) of a program in a manner intended to expose errors efficiently. Experimental results show the utility of this class of heuristics. In contrast to these very general heuristics, we also present very lightweight techniques for introducing program-specific heuristic guidance.

Keywords: Model checking - Heuristic search - Coverage metrics - Testing

Directed Error Detection in C++

Peter Leven, Tilman Mehler and Stefan Edelkamp: Directed Error Detection in C++ with the Assembly-Level Model Checker StEAM, Model Checking Software, 2004, LNCS Volume 2989/2004, Pages 39-56, Springer Berlin / Heidelberg
Abstract:
Most approaches for model checking software are based on the generation of abstract models from source code, which may greatly reduce the search space, but may also introduce errors that are not present in the actual program.
In this paper, we propose a new model checker for the verification of native C++-programs. To allow platform independent model checking of the object code for concurrent programs, we have extended an existing virtual machine for C++ to include multi-threading and different exploration algorithms on a dynamic state description.
The error reporting capabilities and the lengths of counter-examples are improved by using heuristic estimator functions and state space compaction techniques that additionally reduce the exploration efforts.
The evaluation of four scalable simple example problems shows that our system StEAM can successfully enhance the detection of deadlocks and assertion violations.

Partial-Order Reduction in Directed Model Checking

Stefan Edelkamp, Stefan Leue, Alberto Lluch-Lafuente: Partial-Order Reduction and Trail Improvement in Directed Model Checking, Software Tools for Technology Transfer (STTT), 2004, Volume 6 (4), Pages 277-301, Springer Berlin / Heidelberg
Abstract:  
In this paper we present work on trail improvement and partial-order reduction in the context of directed explicit-state model checking. Directed explicit-state model checking employs directed heuristic search algorithms such as A* or best-first search to improve the error-detection capabilities of explicit-state model checking. We first present the use of directed explicit-state model checking to improve the length of already established error trails. Second, we show that partial-order reduction, which aims at reducing the size of the state space by exploiting the commutativity of concurrent transitions in asynchronous systems, can coexist well with directed explicit-state model checking. Finally, we illustrate how to mitigate the excessive length of error trails produced by partial-order reduction in explicit-state model checking. In this context we also propose a combination of heuristic search and partial-order reduction to improve the length to already provided counterexamples.

Keywords:  Model checking - Heuristic search - Trail improvement - Partial-order reduction - HSF-SPIN