Search and Partial Coverage: A model checker can be used to verify the correctness of a finite-state system with respect to a desired property by searching a labeled state-transition graph that models the system to see whether it satisfies the property specified in some notation (e.g., as a Linear Temporal Logic (LTL) formula).
After running a model checker on the target application model there can be two main outcomes. Either the tool finds one or more violations of the specified property or it does not. If it finds such a violation, the tool typically returns a counterexample—a trace of program execution—which shows how it occurred. The user can then use the results to locate and fix the problem.
On the other hand, the model checker might not find such violations. Instead, it might:
- Finish and report that its work is complete and no violations were detected;
- Die before completing because it ran out of system resources such as memory; or
- Get lost in the vast state space and seem to be running indefinitely (the execution takes too long with no sign of the light at the end of the tunnel).