Combining Model Checking and Testing for Software Analysis

Software systems are used widely in many applications where a bug in the system can cause large damage. To prove the correctness of the software system by finding the bugs is the most important and the most difficult task. In this paper, we review and discuss the current approaches for software analysis mainly on model checking and testing. Model checking is a proven successful technology but it works on only finite state machines while most software systems have infinitely many states. Therefore model checking must be performed on rather abstract models. Due to the possible mistakes induced in the modeling process, the bugs found in the model during its verification may not correspond to real errors in the code. To solve this modeling problem, we advocate the need for a unified approach that combines the strengths of both model checking and software testing. Another solution is to automatically extract the model from the source code. We also outline the possible research directions in software verification area.