Département d'informatique, IC - Section d'informatique IC-SIN (Laboratoire de génie logiciel LGL)

Formal testing of object-oriented software : from the method to the tool

Péraire, Cécile ; Strohmeier, Alfred (Dir.)

Thèse Ecole polytechnique fédérale de Lausanne EPFL : 1998 ; no 1904.

Add to personal list
    Summary
    This thesis presents a method and a tool for test set selection, dedicated to object-oriented applications and based on formal specifications. Testing is one method to increase the quality of today’s extraordinary complex software. The aim is to find program errors with respect to given criteria of correctness. In the case of formal testing, the criterion of correctness is the formal specification of the tested application: program behaviors are compared to those required by the specification. In this context, the difficulty of testing object-oriented software arises from the fact that the behavior of an object does not only depend on the input values of the parameters of its operations, but also on its current state, and generally on the current states of other related objects. This combinatorial explosion requires carefully selecting pertinent test sets of reasonable size. This thesis proposes a formal testing method which takes this issue into account. Our approach is based on two different formalisms: a specification language well adapted to the expression of system properties from the specifier’s point of view, and a test language well adapted to the description of test sets from the tester’s point of view. Specifications are written in an object-oriented language, CO-OPN (Concurrent Object-Oriented Petri Nets), based on synchronized algebraic Petri nets and devoted to the specification of concurrent systems. Test sets are expressed using a very simple temporal logic, HML (Hennessy-Milner Logic), whose logic formulas can be executed by a program. There exists a full agreement, shown in this thesis, between the CO-OPN and HML satisfaction relationships: the program satisfies its specification if and only if it satisfies the exhaustive test set derived from this specification. The exhaustive test set expresses all the specification properties. The exhaustive test set is generally infinite. Its size is reduced by applying hypotheses to the program behavior. These hypotheses define test selection strategies and reflect common test practices. The quality of the test sets thus selected only depends on the pertinence of the hypotheses. Concretely, the reduction is achieved by associating to each hypothesis applied to the program, a constraint on the test set. Our method proposes a set of elementary constraints: syntactic constraints on the structure of the tests and semantic constraints which allow to instantiate the test variables so as to cover the different classes of behaviors induced by the specification (subdomain decomposition). Elementary constraints can be combined to form complex constraints. Finally, the constraint system defined on the exhaustive test set is solved, and the solution leads to a pertinent test set of reasonable size. Thanks to the CO-OPN semantics, which allows to compute all the correct and incorrect behaviors induced by a specification, our method is able to test, on the one hand that a program does possess correct behaviors, and on the other hand that a program does not possess incorrect behaviors. An advantage of this approach is to provide through the tests, an observational description of valid and invalid implementations. Our testing method exhibits the advantage of being formal, and thus allows a semi-automation of the test selection process. A new tool, called CO-OPNTEST, is presented in this thesis. This tool assists the tester during the construction of constraints to apply to the exhaustive test set; afterward it automatically generates a test set satisfying these constraints. The CO-OPNTEST architecture is composed of a PROLOG kernel and a Java graphical interface. The kernel is an equational resolution procedure based on logic programming. It includes control mechanisms for subdomain decomposition. The graphical interface allows a user-friendly definition of the test constraints. The CO-OPNTEST tool has generated test sets for several case studies in a simple, rapid and efficient way. In particular, it has generated test sets for an industrial case study of realistic size: the control program of a production cell [Lewerentz 95]. CO-OPNTEST and its application to significant examples demonstrate the pertinence of our approach.
    Résumé
    Ce mémoire présente une méthode et un outil d'assistance à la sélection de jeux de tests, dédiés aux applications orientées-objets et basés sur les spécifications formelles. Le test est une des méthodes permettant d'augmenter la qualité des logiciels extraordinairement complexes d'aujourd'hui. L'objectif du test est de trouver les erreurs d'un programme par rapport à un certain critère de correction. Dans le cas du test formel, le critère de correction est la spécification de l'application testée: les comportements du programme sont comparés aux comportements requis par la spécification. Dans ce contexte, la difficulté de tester des logiciels orientés-objets provient du fait que le comportement d'un objet ne dépend pas uniquement des valeurs d'entrée des paramètres de ses opérations, mais également de l'état courant de l'objet, et généralement de l'état courant d'autres objets du système référencés par ce dernier. Cette explosion combinatoire implique de sélectionner avec soin des jeux de tests pertinents de taille raisonnable. Ce mémoire propose une méthode de test formel qui tient compte de ces difficultés. Notre approche est basée sur deux formalismes distincts: un langage de spécification bien adapté à l'expression des propriétés du système du point de vue du concepteur, et un langage de test bien adapté à la description de jeux de tests du point de vue du testeur. Les spécifications sont rédigées dans un langage orienté-objets (CO-OPN, Concurrent Object-Oriented Petri Nets) basé sur les réseaux de Petri algébriques synchronisés et dédié à la spécification de systèmes concurrents. Les jeux de tests sont exprimés à l'aide d'une logique temporelle très simple (HML, Hennessy-Milner Logic) dont les formules logiques peuvent être exécutées par un programme. Il existe une adéquation, démontrée dans ce mémoire, entre les relations de satisfaction de CO-OPN et HML: le programme satisfait sa spécification si, et seulement si, il satisfait le jeu de tests exhaustif dérivé de cette spécification. Le jeu de tests exhaustif exprime l'ensemble des propriétés de la spécification, il est généralement infini, mais sa taille peut être réduite en faisant des hypothèses sur le comportement du programme. Ces hypothèses définissent des stratégies de sélection de tests et reflètent des pratiques courantes. La qualité des jeux de tests ainsi sélectionnés dépend uniquement de la pertinence des hypothèses. Concrètement, cette réduction est réalisée en associant à chaque hypothèse sur le comportement du programme, une contrainte sur le jeu de tests. Notre méthode propose un éventail de contraintes élémentaires: contraintes syntaxiques sur la structure des tests, et contraintes sémantiques visant à assigner les variables des tests de manière à couvrir les différentes classes de comportements induites par la spécification (décomposition en sous-domaines). Ces contraintes élémentaires peuvent être combinées afin de former des contraintes plus complexes. Finalement, le système de contraintes défini sur le jeu de tests exhaustif est résolu, et la solution mène à un jeu de tests pertinent de taille raisonnable. Grâce à la sémantique de CO-OPN, qui permet de calculer l'ensemble des comportements corrects et incorrects induits par une spécification, notre méthode permet de vérifier, d'une part qu'un programme possède des comportements corrects, et d'autre part qu'il ne possède pas de comportement incorrect. L'avantage de cette approche est de fournir une description observable des implémentations valides et non-valides par le biais des tests. Notre méthode de test repose sur des bases formelles permettant une semi-automatisation du processus de sélection de tests. Un nouvel outil, CO-OPNTEST, est présenté dans ce mémoire. Cet outil assiste le testeur durant la construction de contraintes à appliquer sur le jeu de tests exhaustif, puis génère un jeu de tests satisfaisant ces contraintes de manière automatique. L'architecture de CO-OPNTEST est composée d'un noyau PROLOG et d'une interface graphique Java. Le noyau est une procédure de résolution équationnelle basée sur la programmation logique. Il inclut des mécanismes de contrôle nécessaires à la décomposition en sous-domaines. L'interface graphique permet une construction conviviale des contraintes de test. L'outil CO-OPNTEST a permis de générer des jeux de tests pour différentes études de cas de manière simple, rapide et efficace. En particulier, il a généré des jeux de tests pour une étude de cas de taille réaliste emprunté au monde industriel: le programme de contrôle d'une cellule de production [Lewerentz 95]. CO-OPNTEST et ses applications sur des exemples significatifs démontrent la pertinence de notre approche.