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.
EPFL1998
