Modélisation par contraintes de programmes en bytecode Java pour la génération automatique de tests

摘要

Program verification is essential to maintain a certain level of quality and reliability. Testing is to date the most used software verification mean in industry. Constraint programming is seen as an effective way to automate test data generation. In this thesis we propose a constraint modeling of the Java bytecode semantics, and a method, based on this modeling, to automatically generate test data. Our constraint model of the semantics of a Java bytecode program allows effective deductions, including in the presence of complex data structures or inheritance. In particular, the use of type variables can take into account inheritance and polymorphic method calls. Our method of test data generation uses the constraint model to cover specific instructions of the program under test. It uses a backward progression in the control flow graph to enumerate paths leading to the target instructions. This method suits particularly to cover instructions that are not reached by other methods of test data generation. Finally this method is implemented in a prototype named JAUT (Java Automatic Unit Testing). The experiments show that the prototype can increase the statements coverage obtained with the other available tools.