Model Checking versus Testing

Question

How can you distinguish Model Checking and Testing. Briefly explain with suitable diagram.

Answer 1

Model Checking vs. Testing: Model checking is often claimed to have an advantage over testing since all possible behaviors of a system are analyzed, the idea being that model checking might catch subtle errors that testing could miss.

The first work linking model checking and testing was to use model checking for test-case generation (Callahan, Schneider, and Easterbrook, 1996; Gargantini and Heitmeyer 1999).

One notable difference between testing and model checking is that model checking is more suited to analysis of concurrent and reactive programs because it has full control over the scheduling of processes, threads, and events, which is not typically the case in testing. Also, because a model checker stores the program states that it has visited (to stop it from getting lost by repeating itself), it can be more efficient in covering the behaviors of a program (Park et al. 2000).

While this is true in theory, real systems tend to have large state spaces, and it is impossible to store all the states of the system. That is the bad news. The good news is that, in case studies involving real systems, errors can usually be revealed by considering just a few subtle interactions, rather than a multitude of complex ones. Looking at only part of the state space (or behaviors) can therefore be effective for finding errors when using a model checker to analyze a real program.