Formal testing of object-oriented software

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.

Stepwise refinement of formal specifications based on logical formulae

One of the steps making it possible to increase the quality and the reliability of the software executing on distributed systems consists of the use of methods of software engineering that are known as formal. The majority of the formal methods currently existing correspond in fact more to formal specifications languages than to methods themselves. This is due to the fact that the two fundamental aspects which are: the logic of use of the language and the coverage of the software life cycle are not, for the majority, defined. The development by stepwise refinement is one of the means making it possible to define these two aspects. This thesis aims to the definition of the concepts of refinement and implementation of model-oriented formal specifications. It brings a methodological base making it possible to use such a specifications language during a development by stepwise refinements and during the implementation stage. This thesis defines, initially, a theoretical framework for the refinement and the implementation of formal specifications. The main idea consists in associating a contract with each specification. A contract explicitly represents the whole of the properties of the specification which it is necessary to preserve at the time of a refinement of this specification. To show that a concrete specification refines some abstract specification, it is then a matter of showing that the contract of the concrete specification is sufficient to ensure the properties corresponding to the contract of the abstract specification. The second part of this thesis consists in applying this theoretical framework in the context of the CO-OPN/2 language. CO-OPN/2 is an object-oriented formal specifications language founded on algebraic specifications and Petri nets. Thus, definitions of the concepts of contracts, refinement and implementation are proposed for this language. The contracts are expressed using the Hennessy-Milner temporal logic (HML). This logic is used in the theory of test provided with language CO-OPN/2. Thus, the verification of the contractual properties, as well as the verification of the stages of refinement are facilitated. Refinement and implementation are controlled semantically by the satisfaction of the contracts; syntactically, a renaming is authorised. We specifically study the implementation using the Java programming language. We show how to specify classes of the Java programming language using language CO-OPN/2, so that the last stage of the process of refinement leads to a specification entirely built using CO-OPN/2 components specifying Java classes. The stage of implementation in the Java language itself is thus facilitated. The third part of this thesis shows how it is possible to practically verify that a CO-OPN/2 specification satisfies its own contract, that a stage of refinement is correctly carried out, and finally that the stage of implementation is correctly performed. These verifications are carried out using the theory of the test provided with language CO-OPN/2. Finally, the last part of this thesis illustrates the cogency of this approach by applying it to a complete and detailed case study. A distributed Java application is developped according to the method introduced for the CO-OPN/2 language. Refinement is guided mainly by the satisfaction of functional requirements and by constraints of design integrating the concept of client/server architecture. Lastly, the stages chosen in the refinement process of this development make it possible to study aspects specific to distributed applications, and to propose generic schemas for the design of such applications.

EPFL1999

Test Selection for Specification-Based Testing of Object-Oriented Software Based on Formal Specifications

Traditional testing techniques cannot be directly applied to object-oriented software systems because of some features of this paradigm, namely history, encapsulation, inheritance and polymorphism. We propose a specification based strategy for test selection to verify the interactions of the methods of an object or of a cluster of objects. Its essence is to perform selection as a reduction process. The exhaustive test set which serves as reference of correctness is transformed into a practicable test set by applying hypotheses on the program under test. The number of cases that must be tested is reduced while preserving the integrity of the test set. The oracle is implemented as an observational equivalence, which allows disregarding the internal representation of objects. Besides analyzing the problems induced by the object-oriented paradigm, the main contribution of the thesis is to present a set of hypotheses specific to object-oriented systems. Regularity hypotheses are m:n generalizations of the program behavior and allow specifying the shape of test cases. Uniformity hypotheses are 1:n generalizations of the program behavior. Used in conjunction with subdomain decomposition, they ensure a good coverage of the specification. Incrementallity hypotheses are applied to take advantage of the hierarchy relationships inside object models by reusing test cases already selected for parent classes to test subclasses. Other hypotheses are proposed to limit the impact of polymorphism by taking into account the properties of the subtyping relationships. For further information, please go to my PhD home page.

1997

Stepwise refinement of formal specifications based on logical formulae

EPFL1999