Integration Testing from Structured First-Order Specifications via Deduction Modulo

Abstract

Testing from first-order specifications has mainly been studied for flat specifications, that are specifications of a single software module. However, the specifications of large software systems are generally built out of small specifications of individual modules, by enriching their union. The aim of integration testing is to test the composition of modules assuming that they have previously been verified, i.e. assuming their correctness. One of the main method for the selection of test cases from first-order specifications, called axiom unfolding, is based on a proof search for the different instances of the property to be tested, thus allowing the coverage of this property. The idea here is to use deduction modulo as a proof system for structured first-order specifications in the context of integration testing, so as to take advantage of the knowledge of the correctness of the individual modules. Testing is a very common practice in the software validation process. The principle of testing is to execute the software system on a subset of its possible inputs in order to detect failures. A failure is detected if the system behaves in a non-conformant way with respect to its specification. The testing process is usually decomposed into three phases: the selection of a relevant subset of the set of all the possible inputs of the system, called a test set; the submission of this test set to the system; the decision of the success or the failure of the test set submission, called the oracle problem. We focus here on the selection phase, which is the crucial point for the relevance and the efficiency of the testing process. In the approach called black-box testing, tests are selected from a (formal or informal) specification of the system, without any knowledge about the implementation. Our work follows the framework defined by Gaudel, Bernot and Marre [1], for testing from specifications expressed in a logical formalism. One approach to selection consists first in dividing an exhaustive test set into subsets, and then in choosing one test case in each of these subsets, thus building a finite test set which covers the initial exhaustive test set. One of the most studied selection method for testing from equational (and then first-order) specifications is known as axiom unfolding [1–4]. Its principle is to divide the initial exhaustive test set according to criteria derived from the axioms of the specification, using the well-known and efficient proof techniques associated to first-order logic. Contribution. Test case selection from first-order specifications have mainly been studied for flat specifications (and then flat programs), that are specifications of a single software module. However, for the description of large systems, it is convenient to compose specifications in a modular way [5]. The specification of a large system is generally built from small specifications of individual modules, that are composed by making their union and enriching it with new features in order to get new (larger) specifications, that are themselves composed and so on. The aim of integration testing is to test the composition of modules, assuming that these modules have previously been tested and then are correct. The assumption here is that the system under test is structured according to the structuration of its specification. Here, we propose to use the knowledge of the correctness of individual modules to make the test selection method based on axiom unfolding more efficient. Since the modules are correct (i.e. they have already been sufficiently tested or completely proved), it is reasonable to assume to have an executable and complete specification of these modules, either from which their implementations has been build or which would have been generated from their implementations. Our selection method being defined for first-order specifications, it is important for this executable specification to be written in first-order logic. Of course, in the case where the specification has to be generated from the implementation, the generation may be more or less easy according to the programming language used (imperative or functional), but this is the price to pay to make the selection method efficient by taking advantage of the specification structure. However, we can observe that the obtained specification is most often composed of (conditional) equations that can be oriented from left to right into confluent and terminating (conditional) rewrite rules, and of predicate definition formulas of the form p(t1, . . . , tn)⇔ φ, where φ is a quantifier-free formula, that can be oriented into confluent and terminating rewrite rules on propositions (see Section 2). We will then suppose to have, for each individual module, a confluent and terminating rewrite system that completely specifies its behaviour. To preserve the black-box aspect of the approach (the tester has no knowledge about the implementation of the system and its modules), we suppose that these executable and complete specifications of modules have been written beforehand by the programmer. In order to make our selection method more efficient, we propose to use the deduction modulo proposed by Dowek, Hardin and Kirchner [6] as a proof system for structured specifications. Deduction modulo is a formalism introduced to separate computations from deductions in proofs by reasoning modulo a congruence on propositions, which is defined by a rewrite relation over first-order terms and propositions. The idea behind deduction modulo is to hide the computational part of the proof in the congruence, in order to focus on its deductive part. In the context of integration testing, the same idea can be used to focus the proof on the new features coming from the composition of modules, relying on the correct behaviour of these modules which is embedded in the congruence. It leads to shorter proofs which take advantage of the structuration of specifications, thus making the selection procedure more efficient. Related Work. Testing from structured first-order specifications has already been studied in the framework of institutions. Machado’s works deal with the oracle problem [7], that is, whether a finite and executable procedure can be defined for interpreting the results of tests. When dealing with structured specifications, problems arise in particular with the union of specifications. Since the same sort and operations may be introduced and specified in different modules, the union will be consistent only if the different specifications of the same operations are. Doche and Wiels define an extension of the notion of institution to take test cases into account [8]. They incrementally generate tests from structured specifications, generating tests from small specifications and composing them according to a push-out of specifications. Both of these works aim at building a general test set for the whole structured specification, composing individual test sets obtained for each of its part. The structuration of the specification helps to incrementally build the test set but not to actually test the program in an incremental way. We are here interested in incrementally testing from a structured specification, basing the construction of a test set on the success of the previous ones. Moreover, from the selection point of view, none of the mentioned works propose any particular strategy, but the substitution of axiom variables for some arbitrarily chosen data. Organisation of the Paper. We first recall standard definitions about structuration of specifications (Section 1) and deduction modulo (Section 2). Section 3 introduces the general framework for testing from logical specifications and gives the result of the existence of an exhaustive test set for quantifier-free first-order specifications. We also prove the existence of an exhaustive test set for structured first-order specifications, relying on the correctness of the smaller modules. We restrict to quantifier-free formulas since we showed in [9] that existential formulas are not testable. Testing a formula of the form ∃xφ(x) actually comes down to exhibiting a witness value a such that φ(a) is interpreted as true by the system. Of course, there is no general way to exhibit such a relevant value, but notice that surprisingly, exhibiting such a value would amount to simply prove the system with respect to the initial property. In Section 4, the selection method by means of selection criteria is presented. We develop in Section 5 our test selection method from structured first-order specifications, by unfolding axioms using deduction modulo. We give the algorithm of the procedure and prove the soundness and completeness of the method, i.e. the preservation of exhaustiveness through unfolding. 1 Structured First-Order Specifications A multi-sorted first-order signature Σ = (S, F, P, V ) is composed of a set of sorts S, a set of operations F , a set of predicates P and a set of variables V over these sorts. TΣ(V ) and TΣ are both S-indexed sets of terms with variables in V and ground terms, respectively, freely generated from variables and operations in Σ and preserving arity of operations. A substitution is any mapping σ : V → TΣ(V ) that preserves sorts. Substitutions are naturally extended to terms with variables. Formulas (or propositions) are built as usual in first-order logic from atomic formulas p(t1, . . . , tn), where p is a predicate and t1, . . . , tn are first-order terms, and Boolean connectives. Here, we only consider quantifier-free formulas. As usual, variables of quantifier-free formulas are implicitly universally quantified. A formula over Σ is said ground if it does not contain variables. Let us denote For(Σ) the set of all formulas over the signature Σ. A model of a signature Σ is a first-order structure giving an interpretation to sorts, operations and predicates of Σ. Mod(Σ) is the set of models of Σ. The satisfaction of a quantifier-free formula φ by a given modelM of Σ is inductively defined on the structure of φ as usual and denoted by M |= φ. Given a set of formulas Ψ over Σ and two modelsM andM′ of Σ, we say thatM is Ψ -equivalent toM′, denoted by M≡Ψ M′, if and only if for every formula φ in Ψ ,M |= φ if and only ifM′ |= φ. Given a specification Sp = (Σ,Ax ), a model M of Σ is a model of Sp if M satisfies all the formulas in Ax . Mod(Sp) is the subset of Mod(Σ) whose elements are the models of Sp. A formula φ over Σ is a semantic consequence of Sp, denoted by Sp |= φ, if and only if every model M of Sp satisfies φ. Sp• is the set of all the semantic consequences of Sp. The semantics of a specification Sp = (Σ,Ax ) is given by its signature Sig(Sp) = Σ and its class of models JSpK = Mod(Sp). The specification building operators allow to write basic (flat) specifications, to make the union of two specifications and to enrich specifications with additional sorts, operation and/or predicate and axioms [5]. In general, small specifications are written, for instance specifying basic operations and predicates for a given sort (Booleans, naturals, lists. . . ), then they are composed by the union operator, and finally enriched by new sorts, operations, predicates and axioms involving several of the initial specifications (empty list, list length, list of the divisors of a natural. . . ). The union and enrichment operators are defined as follows.

Topics

    0 Figures and Tables

      Download Full PDF Version (Non-Commercial Use)