Test Template Framework - AbsoluteAstronomy.com

The Test Template Framework (TTF) is a model-based testing

Model-based testing

Model-based testing is the application of Model based design for designing and optionally executing the necessary artifacts to perform software testing. Models can be used to represent the desired behavior of the System Under Test , or to represent the desired testing strategies and testing...

(MBT) framework proposed by Phil Stocks and David Carrington in . Although the TTF was meant to be notation-independent, the original presentation was made using the Z formal notation

Z notation

The Z notation , named after Zermelo–Fraenkel set theory, is a formal specification language used for describing and modelling computing systems. It is targeted at the clear specification of computer programs and computer-based systems in general.-History:...

. It is one of the few MBT frameworks approaching unit testing.

Introduction

The TTF is a specific proposal of model-based testing

Model-based testing

(MBT). It considers models to be Z specifications

Z notation

. Each operation within the specification is analyzed to derive or generate abstract test cases. This analysis consists of the following steps:'

Define the input space (IS) of each operation.
Derive the valid input space (VIS) from the IS of each operation.
Apply one or more testing tactics, starting from each VIS, to build a testing tree for each operation. Testing trees are populated with nodes called test classes.
Prune each of the resulting testing trees.
Find one or more abstract test cases from each leaf in each testing tree.

One of the main advantages of the TTF is that all of these concepts are expressed in the same notation of the specification, i.e. the Z notation

Z notation

. Hence, the engineer has to know only one notation to perform the analysis down to the generation of abstract test cases.

Input space

Let

be a Z operation. Let

be all the input and (non-primed) state variables referenced in

, and

their corresponding types. The Input Space (IS) of

, written

, is the Z schema box defined by

Valid input space

Let

be a Z operation. Let

be the precondition

Precondition

In computer programming, a precondition is a condition or predicate that must always be true just prior to the execution of some section of code or before an operation in a formal specification....

. The Valid Input Space (VIS) of

, written

, is the Z schema box defined by

Test class

Let

be a Z operation and let

be any predicate depending on one or more of the variables defined in

. Then, the Z schema box

is a test class of

. Note that this schema is equivalent to

. This observation can be generalized by saying that if

is a test class of

, then the Z schema box defined by

is also a test class of

. According to this definition the VIS is also a test class.

If

is a test class of

, then the predicate

is said to be the characteristic predicate of

is characterized by

.

Test classes are also called test objectives , test templates and test specifications.

Testing tactic

In the context of the TTF a testing tactic is a means to partition

Partition of a set

In mathematics, a partition of a set X is a division of X into non-overlapping and non-empty "parts" or "blocks" or "cells" that cover all of X...

any test class of any operation. However, some of the testing tactics used in practice actually do not always generate a partition of some test classes.

Some testing tactics originally proposed for the TTF are the following:

Disjunctive Normal Form
Disjunctive normal form
In boolean logic, a disjunctive normal form is a standardization of a logical formula which is a disjunction of conjunctive clauses. As a normal form, it is useful in automated theorem proving. A logical formula is considered to be in DNF if and only if it is a disjunction of one or more...

(DNF). By applying this tactic the operation is written in Disjunctive Normal Form
Disjunctive normal form
In boolean logic, a disjunctive normal form is a standardization of a logical formula which is a disjunction of conjunctive clauses. As a normal form, it is useful in automated theorem proving. A logical formula is considered to be in DNF if and only if it is a disjunction of one or more...

and the test class is divided in as many test classes as terms are in the resulting operation's predicate. The predicate added to each new test class is the precondition
Precondition
In computer programming, a precondition is a condition or predicate that must always be true just prior to the execution of some section of code or before an operation in a formal specification....

of one of the terms in the operation's predicate.

Standard Partitions (SP). This tactic uses a predefined partition of some mathematical operator . For example, the following is a good partition for expresions of the form where is one of , and (see Set theory
Set theory
Set theory is the branch of mathematics that studies sets, which are collections of objects. Although any type of object can be collected into a set, set theory is applied most often to objects that are relevant to mathematics...

).

As can be noticed, standard partitions might change according to how much testing the engineer wants to perform.

Sub-domain Propagation (SDP). This tactic is applied to expressions containing:

Two or more mathematical operators for which there are already defined standard partitions, or
Mathematical operators which are defined in terms of other mathematical operators.

In any of these cases, the standard partitions of the operators appearing in the expression or in the definition of a complex one, are combined to produce a partition for the expression. If the tactic is applied to the second case, then the resulting partition can be considered as the standard partition for that operator. Stocks and Carrington in illustrate this situation with

, where

means domain anti-restriction, by giving standard partitions for

and

and propagating them to calculate a partition for

Specification Mutation (SM). The first step of this tactic consists in generating a mutant of the Z operation. A mutant of a Z operation is similar in concept to a mutant of a program, i.e. it is a modified version of the operation. The modification is introduced by the engineer with the intention of uncovering an error in the implementation. The mutant should be the specification that the engineer guesses the programmer has implemented. Then, the engineer has to calculate the subset of the VIS that yields different results in both specifications. The predicate of this set is used to derive a new test class.

Some other testing tactics that may also be used are the following:

In Set Extension (ISE). It applies to predicates of the form . In this case, it generates test classes such that a predicate of the form is added to each of them.

Mandatory Test Set (MTS). This tactic associates a set of constant values to a VIS' variable and generates as many test classes as elements are in the set. Each test class is characterized by a predicate of the form where is the name of the variable and is one of the values of the set.

Numeric Ranges (NR). This tactic applies only to VIS' variables of type (or its "subtype" ). It consists in associating a range to a variable and deriving test classes by comparing the variable with the limits of the range in some ways. More formally, let be a variable of type and let be the associated range. Then, the tactic generates the test classes characterized by the following predicates: , , , , .

Free Type (FT). This tactic generates as many test classes as elements a free (enumerated) type has. In other words, if a model defines type and some operation uses of type , then by applying this tactic each test class will by divided into three new test classes: one in which equals , the other in which equals , and the third where equals .

Proper Subset of Set Extension (PSSE). This tactic uses the same concept of ISE but applied to set inclusions. PSSE helps to test operations including predicates like . When PSSE is applied it generates test classes where a predicate of the form with and , is added to each class. is excluded from because is a proper subset of .

Subset of Set Extension (SSE). It is identical to PSSE but it applies to predicates of the form in which case it generates by considering also .

Testing tree

The application of a testing tactic to the VIS generates some test classes. If some of these test classes are further partitioned by applying one or more testing tactics, a new set of test classes is obtained. This process can continue by applying testing tactics to the test classes generated so far. Evidently, the result of this process can be drawn as a tree

Tree (data structure)

In computer science, a tree is a widely-used data structure that emulates a hierarchical tree structure with a set of linked nodes.Mathematically, it is an ordered directed tree, more specifically an arborescence: an acyclic connected graph where each node has zero or more children nodes and at...

with the VIS as the root node, the test classes generated by the first testing tactic as its children, and so on. Furthermore, Stocks and Carrington in propose to use the Z notation to build the tree, as follows.

Pruning testing trees

In general a test class' predicate is a conjunction of two or more predicates. It is likely, then, that some test classes are empty because their predicates are contradictions. These test classes must be pruned from the testing tree because they represent impossible combinations of input values, i.e. no abstract test case can be derived out of them.

Abstract test case

An abstract test case is an element belonging to a test class. The TTF prescribes that abstract test cases should be derived only from the leaves of the testing tree. Abstract test cases can also be written as Z schema boxes. Let