Evaluation symbolique à contraintes pour la validation : application à Java/JML
Institution:
BesançonDisciplines:
Directors:
Abstract EN:
The work presented in this thesis falls into the domain of formal methods, and especially, in the validation of object-oriented models and programs, respectively achieved by performing symbolic animation and conformance testing. These results focus on the interpretation of formal specifications written in java modeling language (jml). It also presents the applications which follow from it. This work is made in the direction of the research led by the tfc team of the lifc since 2001. It aims at taking into account the jml notation and integrating it within the bz-testing-tools framework. It has required some evolutions within the constraint interpretation mechanism, in order to preserve the java/jml semantics. Therefore, we have worked in two steps. The first step consists in defining a set-thoeretic representation of the java data model that makes it possible to represent the states of a java program by using constraint systems. The second step is performed by expressing the method specifications describing the transitions between the states. The results we obtained in the animation of the jml specifications makes it possible to validate them so that they can be used for the computation of functional test cases. Therefore, a methodology is presented in this document describing the automated boundary test generation from jml specifications. This work has been implemented into a prototype, called jml-testing-tools, which allows the symbolic animation of a jml model and the test cases generation for its corresponding java code.
Abstract FR:
Les travaux presentes dans cette these se situent dans le cadre des methodes formelles, et plus particulierement dans le domaine de la validation de modeles et de programmes orientes objet. La validation est respectivement realisee par animation symbolique et par des techniques de generation de tests de conformite. Les resultats presentes dans ce memoire se focalisent sur l'interpretation a contraintes de specifications ecrites en java modeling language (jml), et aux applications qui en decoulent. Ces travaux se situent dans la continuite des recherches menees dans l'equipe tfc du lifc depuis 2001. Nous nous s'interessons tout particulierement a la prise en compte de la notation jml et a son integration dans l'environnement bz-testing-tools. Celle-ci a necessite des evolutions dans le mecanisme d'interpretation a contraintes, de maniere a respecter la semantique de java/jml. Pour cela, nous avons travaille en deux etapes. La premiere etape consiste a definir une representation logico-ensembliste du modele de donnees java, permettant ainsi la modelisation des etats d'un programme java par un systeme de contraintes. Dans la seconde etape, nous proposons l'expression des specifications de methodes decrivant les transitions entre deux etats du systeme. Les resultats obtenus sur l'animation du modele permettent de valider celui-ci dans l'objectif de produire des cas de tests fonctionnels. Pour ce faire, une methodologie de generation de cas de tests aux limites pour un modele objet est presentee dans ce memoire. Ces travaux ont ete implantes dans un prototype, nomme jml-testing-tools, qui permet l’animation symbolique d’un modele jml et la generation de cas de tests.