Modélisation par contraintes de programmes en bytecode java pour la génération automatique de tests / Florence Charreteur Schadle ; [sous la dir. de] Thomas Jensen, Arnaud Gotlieb

Date :

Editeur / Publisher : [S.l.] : [s.n.] , 2010

Type : Livre / Book

Type : Thèse / Thesis

Langue / Language : français / French

Java (langage de programmation)

Logiciels -- Essais

Logiciels -- Vérification

Jensen, Thomas (1965-.... ; chercheur en informatique) (Directeur de thèse / thesis advisor)

Gotlieb, Arnaud (19..-....) (Directeur de thèse / thesis advisor)

Université de Rennes 1 (1969-2022) (Organisme de soutenance / degree-grantor)

Université européenne de Bretagne (2007-2016) (Autre partenaire associé à la thèse / thesis associated third party)

École doctorale Mathématiques, télécommunications, informatique, signal, systèmes, électronique (Rennes) (Ecole doctorale associée à la thèse / doctoral school)

Résumé / Abstract : La vérification des programmes est indispensable pour maintenir un certain niveau de qualité et de fiabilité. Le test est à ce jour le moyen de vérification des logiciels le plus utilisé dans l’industrie. La programmation par contraintes est vue comme un moyen efficace pour automatiser la génération de données de test. Dans cette thèse nous proposons une modélisation par contraintes de la sémantique du bytecode Java, ainsi qu’une méthode, basée sur cette modélisation, pour générer automatiquement des données de test. Notre modèle à contraintes de la sémantique d’un programme en bytecode Java permet de faire des déductions efficaces, y compris en présence de structures de données complexes ou d’héritage. En particulier, l’utilisation de variables de type permet de prendre en compte l’héritage et les appels de méthodes polymorphes. Notre méthode de génération de données de test exploite le modèle à contraintes pour couvrir des instructions particulières du programme sous test. Elle se base sur un parcours en arrière du graphe de flot de contrôle pour énumérer des chemins menant aux instructions cibles. Elle est en particulier adaptée à la couverture d’instructions non couvertes par les autres méthodes de génération de données de test. Enfin cette méthode est mise en application dans un prototype, JAUT (Java Automatic Unit Testing). Les expériences montrent que le prototype permet d’augmenter la couverture des instructions obtenue avec les autres outils disponibles.

Résumé / Abstract : 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. Ourconstraint model of the semantics of a Java bytecode program allows to make effective deductions, including 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. This method is in particular a good way 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.