Model-Checking Techniques for Testing
From PUMA Graduiertenkolleg
In the software industry, quality assurance is nowadays mainly achieved by testing. The quality of a test depends crucially on the set of employed test cases. But a fundamental weakness of testing remains: it can discover bugs, but does not completely rule them out. On the other hand, model-checking is an approach that proves the absence of bugs. As the correctness problem is undecidable for arbitrary programs, suitable restrictions of the problem need to be considered. Still, model-checking sometimes takes a lot of time.
In earlier works we have developed the tool jMoped, which checks procedural Java programs. If the user sets a bound on the size of the heap and the variables used, jMoped is able to decide if all executions that stay within those bounds are correct. Thus one can regard an execution of jMoped as a symbolic execution of the program (for a large set of inputs). jMoped also shows the program points reachable with the considered inputs, i.e., it indicates the degree of coverage which is also an important metrics in testing.
That leads to the question how this interrelation between testing and model-checking can be further exploited, in order, e.g., to extend jMoped to a tool that effectively supports the testing process. It would be interesting to investigate how jMoped can automatically and efficiently identify a set of inputs that leads to a high degree of coverage. Currently such a process still needs to be guided manually by the user. To achieve this goal, the reachability algorithms of jMoped would need to be modified to search specifically for inputs that lead to instructions not yet covered, e.g. by using techniques such as guided search or by a suitable combination of forward and backward search.
A further goal in designing test cases is to examine as many boundary cases as possible to reveal bugs. Automating this process is desirable because there are often many boundary cases that are not obvious at first glance. That raises the question if jMoped can help to retrieve boundary cases. In our experience jMoped can find, even with small bounds, many boundary cases. The performance of jMoped for that purpose could be improved if the analysis could be restricted to interesting boundary cases, which, in turn, should be identified by means of static analysis techniques.
see "Christian Kern"