Model Checking Vs. Testing

Introduction:

• Model checking is a technique for verifying finite-state models of reactive computing systems for proper behavior. The intuitive notion of ‘proper behavior’ is, in turn, formalized through the use of either temporal logic (e.g., linear-time temporal logic) or automata (e.g., B¨uchi automata) which are used to express the desired properties of these systems. In contrast, testing is a well-established and expansive area central to product integrity, and employs both formal and informal criteria for coverage. Neither approach excludes the other; in fact, some of the most promising recent results are in combining model checking and testing ideas.
• Traditional testing-based debugging methods are known to miss bugs due to many reasons. Typical systems being tested contain an astronomical number of states: 2109 states, for instance, in a memory of capacity 1MB! While engineers are known to hand-simplify designs before testing them, in model checking, such simplifications are often done much more aggressively, to the point of turning control branches into nondeterministic selections. Such simplifications help abstract (or “smoothen”) the state-space modeled. BDDs, and many other symbolic representation methods for state spaces, have the (curious) property that by adding more information (which helps overapproximate state spaces, perhaps by adding some infeasible states) the actual BDD sizes are dramatically reduced. Hence, even though the number of states modeled may increase, the memory for representing the states diminishes.
• Two additional important benefits due to the use of nondeterminism are: (i) failure possibilities are introduced without increasing model or state-space sizes, and (ii) the effect of testing for all values of certain critical system parameters is obtained through nondeterminism. Of course these benefits come at a cost, and a designer who understands this cost/benefit ratio can often swing the overall balance in favor of benefit. To understand these discussions, consider the process of debugging of a concurrent system that uses a ‘send’ communication primitive in a library. Assume that send uses a FIFO buffer, and would block if the buffer were to be full. Further, suppose that such blocked sends are considered errors. If one were to allocate a certain number of buffer locations and test in the traditional sense, one would have to wait for the right combinations of global states to arise in which the send buffer in question becomes full, and then only be able to observe the error. Furthermore, the input/state combinations under which this error can be observed during testing may differ from those in the real system because, clearly, the designer would have downscaled all system parameters before testing begins. To make matters worse, it is easy to eliminate errors while downscaling systems in an ad hoc manner.
• In contrast to the testing approach described above, a model checking based approach to solving the same problem would consist of: (i) not modeling buffer capacities, and (ii) nondeterministically triggering a buffer full condition at every possible point in the state-space (this is called over-approximation of the reachable state-space). The advantage of this approach is that all possible buffer capacities are being simulated in one fell swoop. The obvious disadvantage of this approach is that a buffer full may be simulated by the nondeterministic selection mechanism when not warranted (e.g., at the very first send), and the test engineer is forced to study and overrule many false alarms reported by the model checker. This is often a small price to be paid for the thoroughness of coverage offered by a model checker, especially given that testing may not be feasible at all. We are really talking about modeling several thousands of lines of actual code (which may be impossible to test in any real sense) by a less than 100-line model checker input description. In this setting, repeated running of model checking and overruling errors is actually feasible. It is possible that, despite the best precautions, over-approximation based model checking can inundate the engineer with false alarms.
• There are many recently emerging solutions to this problem, the most important of which is an approach based on abstraction refinement. This approach promises to enhance the power of model checking, while helping us handle larger models and at the same time avoiding inaccuracies arising due to hand abstractions created by the designer. In the counterexample guided abstraction refinement (CEGAR) approach for abstraction/refinement, the initial abstraction is deliberately chosen to be too coarse. This abstraction is successively refined by heuristically discovering aspects of the system which need to be captured in detail. The end result is often that systems are verified while keeping much of their behavior highly abstract, thus reducing the overall complexity of verification.