Advantages of Model Checking: Many tools already exist to help detect problems in source code. Testing is clearly the most widely used technique and there are a variety of tools which support test data selection, test case management, test result checking, and test coverage assessment (Bezier 1990; Kaner, Falk, and Nguyen 1993). A growing number of static analysis tools can also evaluate source code for defects without actually executing the code. The capabilities of these tools range from checking simple coding conventions to detecting issues such as non-initialized variables, null pointer dereferences, and array out-of-bounds errors (Coverity; FindBugs; GrammaTech’s CodeSonar; Klocwork; Parasoft’s C++Test and JTest; Polyspace; Evans 1996; Dor, Rodeh, and Sagiv 1998).
For model checking to be useful in practice, it must provide clear benefits over other techniques such as testing and static analysis, either by finding more or different types of errors or by reducing cost.
One area where model checking shows benefits is in concurrent (multithreaded) systems. Testing concurrent systems is problematic because the tester has little control over thread scheduling, and concurrency errors are notoriously irreproducible (Yang, Souter, and Pollock 1998; Hwang, Tai, and Hunag, 1995). Static analysis has had better success dealing with concurrency, but it can be challenging to obtain accurate results
(Naumovich, Avrunin, and Clarke 1999).
Model checking overcomes the two limitations of testing by providing control over the order of thread scheduling and error traces to make test results repeatable. By controlling thread scheduling, the model checker can evaluate any—and sometimes every—possible interleaving of threads in the system.
Another area where model checking can help is in the development of test cases. In addition to controlling thread scheduling, the model checker controls the test environment where the test data originates. Without any guidance, a model checker will naively try to generate all combinations of environmental behaviors as the closed application + environment system is checked. While in practice it is not possible to exhaust all possible inputcombinations, this ideal provides a comprehensive starting point to some new and interesting heuristics for generating test sets. In addition, because the tool itself generates the combinations of inputs, model-checking tools provide some nice techniques for building concise specifications of possible test data values. A model checker can provide much better coverage of the program because it can exhaustively and systematically look at all the possible behaviors rather than selected behaviors chosen (sometimes randomly) by QA personnel.
Even when using the more traditional techniques to come up with a comprehensive set of test cases independently, there still remain the issues of performance and limited system resources available to apply those test cases. Model checkers employ various techniques for backtracking and efficient storage of visited states to avoid revisiting the previously checked portions of the state space. This allows them to be much more efficient with respect to precious resources such as memory and time. It also allows them to provide a trace that records all the significant events along the execution path that lead to an erroneous condition, showing not only what the error was but also how it occurred.
Unlike other available techniques, a model checker can perform these tasks automatically for the most part, if the system is finite-state. Many interesting properties can be verified by a model checker out of the box without requiring much specific domain knowledge or expertise. (Specification of application-specific properties, of course, requires domain expertise.)
It is this exhaustive, systematic, efficient, and automated nature of model checking that makes it attractive for those involved in software verification and validation, and can offer higher levels of assurance compared to other currently available techniques.