The Test Template Framework (TTF) is a model-based testing (MBT) framework proposed by Phil Stocks and David Carrington in for the purpose of software testing. Although the TTF was meant to be notation-independent, the original presentation was made using the Z formal notation. It is one of the few MBT frameworks approaching unit testing.
The TTF is a specific proposal of model-based testing (MBT). It considers models to be Z specifications. Each operation within the specification is analyzed to derive or generate abstract test cases. This analysis consists of the following steps:
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. Hence, the engineer has to know only one notation to perform the analysis down to the generation of abstract test cases.
In this section the main concepts defined by the TTF are described.
Let
Op
x1...xn
Op
T1...Tn
Op
ISOp
[x1:T1...xn:Tn]
Let
Op
preOp
Op
Op
VISOp
[ISOp|preOp]
Let
Op
P
VISOp
[VISOp|P]
Op
[ISOp|preOp\landP]
COp
Op
[COp|P]
Op
If
COp
Op
P
C'Op==[COp|P]
C'Op
C'Op
P
Test classes are also called test objectives, test templates and test specifications.
In the context of the TTF a testing tactic[1] is a means to partition 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:
S\spadesuitT
\spadesuit
\cup
\cap
\setminus
\begin{array}{l|l} S=\emptyset,T=\emptyset&S ≠ \emptyset,T ≠ \emptyset,S\subsetT\\ \hline S=\emptyset,T ≠ \emptyset&S ≠ \emptyset,T ≠ \emptyset,T\subsetS\\ \hline S ≠ \emptyset,T=\emptyset& S ≠ \emptyset,T ≠ \emptyset,T=S\\ \hline S ≠ \emptyset,T ≠ \emptyset,S\capT=\emptyset& S ≠ \emptyset,T ≠ \emptyset,S\capT ≠ \emptyset,lnot(S\subseteqT),lnot(T\subseteqS),S ≠ T \end{array}
As can be noticed, standard partitions might change according to how much testing the engineer wants to perform.
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
R ⊕ G=(domG\ntriangleleftR)\cupG
\ntriangleleft
\ntriangleleft
\cup
⊕
Some other testing tactics that may also be used are the following:
expr\in\{expr1,...,exprn\}
expr=expri
var=val
Z
N
Z
[i,j]
n<i
n=i
i<n\landn<j
n=j
n>j
expr\subset\{expr1,...,exprn\}
2n-1
expr=Ai
i\in[1,2n-1]
Ai\inP\{expr1,...,exprn\}\setminus\{\{expr1,...,exprn\}\}
\{expr1,...,exprn\}
P\{expr1,...,exprn\}
\{expr1,...,exprn\}
expr\subseteq\{expr1,...,exprn\}
2n
\{expr1,...,exprn\}
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 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.
\begin{align} VIS&==[IS|
1 | |
P]\\ TCL | |
T1 |
&==[VIS|
1 | |
P | |
T1 |
n | |
]\\ &...\\ TCL | |
T1 |
&==[VIS|
n | |
P | |
T1 |
1 | |
]\\ TCL | |
T2 |
&==
i | |
[TCL | |
T1 |
|
1 | |
P | |
T2 |
m | |
]\\ &...\\ TCL | |
T2 |
&==
i | |
[TCL | |
T1 |
|
m | |
P | |
T2 |
1 | |
]\\ &...\\ TCL | |
T3 |
&==
j | |
[TCL | |
T2 |
|
1 | |
P | |
T3 |
k | |
]\\ &...\\ TCL | |
T3 |
&==
j | |
[TCL | |
T2 |
|
k | |
P | |
T3 |
]\\ &...\\ &...\\ &... \end{align}
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.
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
Op
VISOp
Op
x1:T1...xn:Tn
VISOp
COp
Op
P1...Pm
COp
VISOp
v1:T1...vn:Tn
n
P1\land...\landPm
COp
[COp|x1=v1\land...\landxn=vn]