|
|
|
@ -6,14 +6,24 @@
|
|
|
|
reference=chap:test-methods]
|
|
|
|
reference=chap:test-methods]
|
|
|
|
|
|
|
|
|
|
|
|
In this chapter we will discuss some of the theory of test generation methods for black box conformance testing.
|
|
|
|
In this chapter we will discuss some of the theory of test generation methods for black box conformance testing.
|
|
|
|
From a theoretical discussion we derive a new algorithm: the \emph{hybrid ADS methods}, which is applied on a case study in the next chapter (\in{Chapter}[chap:applying-automata-learning]).
|
|
|
|
Since the systems we consider are black box, we cannot simply determine equivalence with a specification.
|
|
|
|
A key aspect of such methods is the size of the obtained test suite.
|
|
|
|
The only way to gain confidence is to perform experiments on the system.
|
|
|
|
On one hand we want to cover as much as the specification as possible.
|
|
|
|
A key aspect of test generation methods is the size and completeness of the test suites.
|
|
|
|
|
|
|
|
On one hand, we want to cover as much as the specification as possible, hopefully ensuring that we find mistakes in any faulty implementation.
|
|
|
|
On the other hand: testing takes time, so we want to minimise the size of a test suite.
|
|
|
|
On the other hand: testing takes time, so we want to minimise the size of a test suite.
|
|
|
|
|
|
|
|
|
|
|
|
The test methods described here are well-known in the literature of FSM-based testing.
|
|
|
|
The test methods described here are well-known in the literature of FSM-based testing.
|
|
|
|
They all share similar concepts, such as \emph{access sequences} and \emph{state identifiers}.
|
|
|
|
They all share similar concepts, such as \emph{access sequences} and \emph{state identifiers}.
|
|
|
|
In this chapter we will define these concepts, relate them with one another and show how to build test suites from these concepts.
|
|
|
|
In this chapter we will define these concepts, relate them with one another and show how to build test suites from these concepts.
|
|
|
|
|
|
|
|
From this theoretical discussion we derive a new algorithm: the \emph{hybrid ADS methods}, which is applied on an industrial case study in \in{Chapter}[chap:applying-automata-learning].
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This chapter starts with the basics: Mealy machines, sequences and what it means to test a black box system.
|
|
|
|
|
|
|
|
Then, starting from \in{Section}[sec:separating-sequences] we define several concepts, such as state identifiers, in order to distinguish one state from another.
|
|
|
|
|
|
|
|
These concepts are then combined in \in{Section}[sec:methods] to derive test suites.
|
|
|
|
|
|
|
|
In a similar vein, we define a novel test method in \in{Section}[sec:hybrid] and we discuss some of the implementation details of the \kw{hybrid-ads} tool.
|
|
|
|
|
|
|
|
We summarise the various test methods in \in{Section}[sec:overview].
|
|
|
|
|
|
|
|
All methods are proven to be $n$-complete in \in{Section}[sec:completeness].
|
|
|
|
|
|
|
|
Finally, in \in{Section}[sec:discussion], we give related work.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
\startsection
|
|
|
|
\startsection
|
|
|
|
@ -131,9 +141,9 @@ $||T|| = \sum\limits_{t \in max(T)} (|t| + 1)$.
|
|
|
|
\startexample[reference=incompleteness]
|
|
|
|
\startexample[reference=incompleteness]
|
|
|
|
{\bf No test suite is complete.}
|
|
|
|
{\bf No test suite is complete.}
|
|
|
|
Consider the specification in \in{Figure}{a}[fig:incompleteness-example].
|
|
|
|
Consider the specification in \in{Figure}{a}[fig:incompleteness-example].
|
|
|
|
This machine will always produce zeroes.
|
|
|
|
This machine will always outputs a cup of coffee -- when given money.
|
|
|
|
For any test suite we can make a faulty implementation which passes the test suite.
|
|
|
|
For any test suite we can make a faulty implementation which passes the test suite.
|
|
|
|
Such an implementation might look like \in{Figure}{b}[fig:incompleteness-example] with $n$ big enough.
|
|
|
|
A faulty implementation might look like \in{Figure}{b}[fig:incompleteness-example], where the machine starts to output bombs after $n$ steps.
|
|
|
|
This shows that no test-suite can be complete and it justifies the following definition.
|
|
|
|
This shows that no test-suite can be complete and it justifies the following definition.
|
|
|
|
|
|
|
|
|
|
|
|
\startplacefigure
|
|
|
|
\startplacefigure
|
|
|
|
@ -145,20 +155,20 @@ This shows that no test-suite can be complete and it justifies the following def
|
|
|
|
\starttikzpicture
|
|
|
|
\starttikzpicture
|
|
|
|
\node[state] (0) {$s_0$};
|
|
|
|
\node[state] (0) {$s_0$};
|
|
|
|
\path[->]
|
|
|
|
\path[->]
|
|
|
|
(0) edge [loop] node [below] {${a}/0$} (0);
|
|
|
|
(0) edge [loop] node [below] {\money $/$ \coffee} (0);
|
|
|
|
\stoptikzpicture
|
|
|
|
\stoptikzpicture
|
|
|
|
}} {(a)}
|
|
|
|
}} {(a)}
|
|
|
|
{\hbox{
|
|
|
|
{\hbox{
|
|
|
|
\starttikzpicture
|
|
|
|
\starttikzpicture[bend angle=20]
|
|
|
|
\node[state] (0) {$s'_0$};
|
|
|
|
\node[state] (0) {$s'_0$};
|
|
|
|
\node[state] (1) [right of=0] {$s'_1$};
|
|
|
|
\node[state] (1) [right of=0] {$s'_1$};
|
|
|
|
\node (2) [right of=1] {$\cdots$};
|
|
|
|
\node (2) [right of=1] {$\cdots$};
|
|
|
|
\node[state] (3) [right of=2] {$s'_n$};
|
|
|
|
\node[state] (3) [right of=2] {$s'_n$};
|
|
|
|
\path[->]
|
|
|
|
\path[->]
|
|
|
|
(0) edge [bend left=20 ] node [below] {${a}/0$} (1)
|
|
|
|
(0) edge [bend left] node [below] {\money $/$ \coffee} (1)
|
|
|
|
(1) edge [bend left=20 ] node [below] {${a}/0$} (2)
|
|
|
|
(1) edge [bend left] node [below] {\money $/$ \coffee} (2)
|
|
|
|
(2) edge [bend left=20 ] node [below] {${a}/0$} (3)
|
|
|
|
(2) edge [bend left] node [below] {\money $/$ \coffee} (3)
|
|
|
|
(3) edge [loop ] node [below] {${a}/1$} (3);
|
|
|
|
(3) edge [loop] node [below] {\money $/$ \bomb} (3);
|
|
|
|
\stoptikzpicture
|
|
|
|
\stoptikzpicture
|
|
|
|
}} {(b)}
|
|
|
|
}} {(b)}
|
|
|
|
\stopcombination
|
|
|
|
\stopcombination
|
|
|
|
@ -173,7 +183,6 @@ We say that $T$ is \emph{$m$-complete (for $M$)} if for all inequivalent machine
|
|
|
|
|
|
|
|
|
|
|
|
We are often interested in the case of $m$-completeness, where $m = n + k$ for some $k \in \naturalnumbers$ and $n$ is the number of states in the specification.
|
|
|
|
We are often interested in the case of $m$-completeness, where $m = n + k$ for some $k \in \naturalnumbers$ and $n$ is the number of states in the specification.
|
|
|
|
Here $k$ will stand for the number of \emph{extra states} we can test.
|
|
|
|
Here $k$ will stand for the number of \emph{extra states} we can test.
|
|
|
|
The issue of an unknown bound is addressed later in the paper.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Note the order of the quantifiers in the above definition.
|
|
|
|
Note the order of the quantifiers in the above definition.
|
|
|
|
We ask for a single test suite which works for all implementations of bounded size.
|
|
|
|
We ask for a single test suite which works for all implementations of bounded size.
|
|
|
|
@ -182,7 +191,8 @@ This is crucial for black box testing, as we do not know the implementation, so
|
|
|
|
|
|
|
|
|
|
|
|
\stopsubsection
|
|
|
|
\stopsubsection
|
|
|
|
\startsubsection
|
|
|
|
\startsubsection
|
|
|
|
[title={Separating Sequences}]
|
|
|
|
[title={Separating Sequences},
|
|
|
|
|
|
|
|
reference=sec:separating-sequences]
|
|
|
|
|
|
|
|
|
|
|
|
Before we construct test suites, we discuss several types of useful sequences.
|
|
|
|
Before we construct test suites, we discuss several types of useful sequences.
|
|
|
|
All the following notions are standard in the literature, and the corresponding references will be given in \in{Section}[sec:methods], where we discuss the test generation methods using these notions.
|
|
|
|
All the following notions are standard in the literature, and the corresponding references will be given in \in{Section}[sec:methods], where we discuss the test generation methods using these notions.
|
|
|
|
@ -228,7 +238,7 @@ As the example shows, we need sets of sequences and sometimes even sets of sets
|
|
|
|
|
|
|
|
|
|
|
|
\startdefinition
|
|
|
|
\startdefinition
|
|
|
|
Given a Mealy machine $M$, we define the following kinds of sets of sequences.
|
|
|
|
Given a Mealy machine $M$, we define the following kinds of sets of sequences.
|
|
|
|
We require that all sets are \emph{prefix-closed}, however, we only give the maximal sequences in examples.
|
|
|
|
We require that all sets are \emph{prefix-closed}, however, we only show the maximal sequences in examples.
|
|
|
|
\footnote{Taking these sets to be prefix-closed makes many proofs easier.}
|
|
|
|
\footnote{Taking these sets to be prefix-closed makes many proofs easier.}
|
|
|
|
\startitemize
|
|
|
|
\startitemize
|
|
|
|
\item A set of sequences $W$ is a called a \defn{characterisation set} if it contains a separating sequence for each pair of distinct states in $M$.
|
|
|
|
\item A set of sequences $W$ is a called a \defn{characterisation set} if it contains a separating sequence for each pair of distinct states in $M$.
|
|
|
|
@ -256,28 +266,38 @@ But note that such a family will \emph{not} be harmonised since the sets $\{ a \
|
|
|
|
\stopexample
|
|
|
|
\stopexample
|
|
|
|
|
|
|
|
|
|
|
|
One more type of state identifier is of our interest: the \emph{adaptive distinguishing sequence}.
|
|
|
|
One more type of state identifier is of our interest: the \emph{adaptive distinguishing sequence}.
|
|
|
|
It it the strongest type of state identifier, and as a result not many machine have one.
|
|
|
|
It it the strongest type of state identifier, and as a result not many machines have one.
|
|
|
|
|
|
|
|
Like DSs, adaptive distinguishing sequences can identify a state using a single word.
|
|
|
|
|
|
|
|
We give a slightly different (but equivalent) definition than the one of \citet[DBLP:journals/tc/LeeY94].
|
|
|
|
|
|
|
|
|
|
|
|
\startdefinition
|
|
|
|
\startdefinition
|
|
|
|
Following the results of \citet[DBLP:journals/tc/LeeY94], a separating family where each set is the prefix-closure of a single word is called an \defn{adaptive distinguishing sequence} (ADS).
|
|
|
|
A separating family $\Fam{H}$ is an \defn{adaptive distinguishing sequence} (ADS) if each set $\max(H_s)$ is a singleton.
|
|
|
|
\stopdefinition
|
|
|
|
\stopdefinition
|
|
|
|
|
|
|
|
|
|
|
|
An ADS is of special interest since they can identify a state using a single word.
|
|
|
|
|
|
|
|
It is called an adaptive sequence, since it has a tree structure which depends on the output of the machine.
|
|
|
|
It is called an adaptive sequence, since it has a tree structure which depends on the output of the machine.
|
|
|
|
To see this, consider the first symbols of each of the sequences in the family.
|
|
|
|
To see this tree structure, consider the first symbols of each of the sequences in the family.
|
|
|
|
Since the family is harmonised and each set is given by a single word, there is only one first symbol.
|
|
|
|
Since the family is harmonised and each set is essentially given by a single word, there is only one first symbol.
|
|
|
|
So we test each state with one symbol, observe the output, and then continue with the remainder of the sequence (which depends on the output).
|
|
|
|
Depending on the output after the first symbol, the sequence continues.
|
|
|
|
\todo{Verwijs naar plaatje}
|
|
|
|
|
|
|
|
Given an ADS, there exists an UIO for every state.
|
|
|
|
|
|
|
|
The converse -- if every state has an UIO, then the machine admits an ADS-- does not hold.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
The machine in \in{Figure}[fig:running-example] admits no ADS, since $s_2$ has no UIO.
|
|
|
|
\startexample
|
|
|
|
|
|
|
|
In \in{Figure}[fig:ads-example] we see a machine with an ADS.
|
|
|
|
|
|
|
|
The ADS is given as follows:
|
|
|
|
|
|
|
|
\startformulas
|
|
|
|
|
|
|
|
\startformula H_0 = \{aba\} \stopformula
|
|
|
|
|
|
|
|
\startformula H_1 = \{aaba\} \stopformula
|
|
|
|
|
|
|
|
\startformula H_2 = \{aba\} \stopformula
|
|
|
|
|
|
|
|
\startformula H_3 = \{aaba\} \stopformula
|
|
|
|
|
|
|
|
\stopformulas
|
|
|
|
|
|
|
|
Note that all sequences start with $a$.
|
|
|
|
|
|
|
|
This already separates $s_0, s_2$ from $s_1, s_3$.
|
|
|
|
|
|
|
|
To further separate the states, the sequences continues with either a $b$ or another $a$.
|
|
|
|
|
|
|
|
And so on.
|
|
|
|
|
|
|
|
|
|
|
|
\startplacefigure
|
|
|
|
\startplacefigure
|
|
|
|
[title={(a): A Mealy machine with alphabets $I = \{a, b\}$ and $O = \{0, 1\}$ and (b): an ADS for (a). },
|
|
|
|
[title={(a): A Mealy machine with an ADS and (b): the tree structure of this ADS. },
|
|
|
|
list={A Mealy machine and its ADS.}
|
|
|
|
list={A Mealy machine and its ADS.},
|
|
|
|
reference=fig:ads-example]
|
|
|
|
reference=fig:ads-example]
|
|
|
|
\startcombination[nx=2, ny=1, align=center]
|
|
|
|
\startcombination[2*1]
|
|
|
|
{\hbox{
|
|
|
|
{\hbox{
|
|
|
|
\starttikzpicture
|
|
|
|
\starttikzpicture
|
|
|
|
\node[initial, state] (0) {$s_0$};
|
|
|
|
\node[initial, state] (0) {$s_0$};
|
|
|
|
@ -296,13 +316,13 @@ The machine in \in{Figure}[fig:running-example] admits no ADS, since $s_2$ has n
|
|
|
|
\node (0) {$a$};
|
|
|
|
\node (0) {$a$};
|
|
|
|
\node [below left=of 0] (1) {$b$};
|
|
|
|
\node [below left=of 0] (1) {$b$};
|
|
|
|
\node [below=of 1] (3) {$a$};
|
|
|
|
\node [below=of 1] (3) {$a$};
|
|
|
|
\node [below left=of 3] (5) {$2$};
|
|
|
|
\node [below left=of 3] (5) {$s_2$};
|
|
|
|
\node [below right=of 3] (6) {$0$};
|
|
|
|
\node [below right=of 3] (6) {$s_0$};
|
|
|
|
\node [below right=of 0] (2) {$a$};
|
|
|
|
\node [below right=of 0] (2) {$a$};
|
|
|
|
\node [below=of 2] (4) {$b$};
|
|
|
|
\node [below=of 2] (4) {$b$};
|
|
|
|
\node [below=of 4] (7) {$a$};
|
|
|
|
\node [below=of 4] (7) {$a$};
|
|
|
|
\node [below left=of 7] (8) {$1$};
|
|
|
|
\node [below left=of 7] (8) {$s_1$};
|
|
|
|
\node [below right=of 7] (9) {$3$};
|
|
|
|
\node [below right=of 7] (9) {$s_3$};
|
|
|
|
|
|
|
|
|
|
|
|
\path[->]
|
|
|
|
\path[->]
|
|
|
|
(0)+(0,.75) edge (0)
|
|
|
|
(0)+(0,.75) edge (0)
|
|
|
|
@ -318,12 +338,42 @@ The machine in \in{Figure}[fig:running-example] admits no ADS, since $s_2$ has n
|
|
|
|
\stoptikzpicture}} {(b)}
|
|
|
|
\stoptikzpicture}} {(b)}
|
|
|
|
\stopcombination
|
|
|
|
\stopcombination
|
|
|
|
\stopplacefigure
|
|
|
|
\stopplacefigure
|
|
|
|
|
|
|
|
\stopexample
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Given an ADS, there exists an UIO for every state.
|
|
|
|
|
|
|
|
The converse -- if every state has an UIO, then the machine admits an ADS -- does not hold.
|
|
|
|
|
|
|
|
The machine in \in{Figure}[fig:running-example] admits no ADS, since $s_2$ has no UIO.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
\stopsubsection
|
|
|
|
|
|
|
|
\startsubsection
|
|
|
|
|
|
|
|
[title={Partial equivalence}]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
\startdefinition
|
|
|
|
|
|
|
|
We define the following notation.
|
|
|
|
|
|
|
|
\startitemize
|
|
|
|
|
|
|
|
\item
|
|
|
|
|
|
|
|
Let $W$ be a set of sequences.
|
|
|
|
|
|
|
|
Two states $x, y$ are \emph{$W$-equivalent}, written $x \sim_W y$, if $\lambda(x, w) = \lambda(y, w)$ for all $w \in W$.
|
|
|
|
|
|
|
|
\item
|
|
|
|
|
|
|
|
Let $\Fam{W}$ be a family.
|
|
|
|
|
|
|
|
Two states $x, y$ are \emph{$\Fam{W}$-equivalent}, written $x \sim_{\Fam{W}} y$, if $\lambda(x, w) = \lambda(y, w)$ for all $w \in X_x \cap X_y$.
|
|
|
|
|
|
|
|
\stopitemize
|
|
|
|
|
|
|
|
\stopdefinition
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Both relations are equivalence relations.
|
|
|
|
|
|
|
|
Moreover, $W \subseteq V$ implies that $V$ separates more states than $W$, i.e., $x \sim_V y \implies x \sim_W y$.
|
|
|
|
|
|
|
|
Clearly, if two states are equivalent (i.e., $s \sim t$), then for any set $W$ we have $s \sim_W t$.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
\stopsubsection
|
|
|
|
|
|
|
|
\startsubsection
|
|
|
|
|
|
|
|
[title={Access sequences}]
|
|
|
|
|
|
|
|
|
|
|
|
\todo{Dit staat een beetje random}
|
|
|
|
|
|
|
|
Besides sequences which separate states, we also need sequences which brings a machine to specified states.
|
|
|
|
Besides sequences which separate states, we also need sequences which brings a machine to specified states.
|
|
|
|
|
|
|
|
|
|
|
|
\startdefinition
|
|
|
|
\startdefinition
|
|
|
|
An \emph{access sequence for $s$} is a word $w$ such that $\delta(q_0, w) = s$.
|
|
|
|
An \emph{access sequence for $s$} is a word $w$ such that $\delta(s_0, w) = s$.
|
|
|
|
A set $P$ consisting of an access sequence for each state is called a \emph{state cover}.
|
|
|
|
A set $P$ consisting of an access sequence for each state is called a \emph{state cover}.
|
|
|
|
If $P$ is a state cover, then $P \cdot I$ is called a \emph{transition cover}.
|
|
|
|
If $P$ is a state cover, then $P \cdot I$ is called a \emph{transition cover}.
|
|
|
|
\stopdefinition
|
|
|
|
\stopdefinition
|
|
|
|
@ -346,11 +396,9 @@ On families we define
|
|
|
|
\startitemize[after]
|
|
|
|
\startitemize[after]
|
|
|
|
\item flattening: $\bigcup \Fam{X} = \{ x \mid x \in X_s, s \in S \}$,
|
|
|
|
\item flattening: $\bigcup \Fam{X} = \{ x \mid x \in X_s, s \in S \}$,
|
|
|
|
\item union: $\Fam{X} \cup \Fam{Y}$ is defined point-wise:
|
|
|
|
\item union: $\Fam{X} \cup \Fam{Y}$ is defined point-wise:
|
|
|
|
$(\Fam{X} \cup \Fam{Y})_s = X_s \cup Y_s$, and
|
|
|
|
$(\Fam{X} \cup \Fam{Y})_s = X_s \cup Y_s$,
|
|
|
|
\item $\Fam{X}$-equivalence:
|
|
|
|
|
|
|
|
$x \sim_\Fam{X} y$ if $\lambda(x,w) = \lambda(y,w)$ for all $w \in X_x \cap X_y$.
|
|
|
|
|
|
|
|
\item concatenation:
|
|
|
|
\item concatenation:
|
|
|
|
$X \odot \Fam{Y} = \{ xy \mid x \in X, y \in Y_{\delta(s_0, x)} \}$ and
|
|
|
|
$X \odot \Fam{Y} = \{ xy \mid x \in X, y \in Y_{\delta(s_0, x)} \}$, and
|
|
|
|
\item refinement: $\Fam{X} ; \Fam{Y}$ defined by
|
|
|
|
\item refinement: $\Fam{X} ; \Fam{Y}$ defined by
|
|
|
|
\startformula
|
|
|
|
\startformula
|
|
|
|
(\Fam{X} ; \Fam{Y})_s = X_s \,\cup\, Y_s \cap \bigcup_{s \sim_{\Fam{X}} t} Y_t.
|
|
|
|
(\Fam{X} ; \Fam{Y})_s = X_s \,\cup\, Y_s \cap \bigcup_{s \sim_{\Fam{X}} t} Y_t.
|
|
|
|
@ -382,6 +430,7 @@ For all families $\Fam{X}$ and $\Fam{Y}$:
|
|
|
|
|
|
|
|
|
|
|
|
In this section, we review the classical conformance testing methods:
|
|
|
|
In this section, we review the classical conformance testing methods:
|
|
|
|
the W, Wp, UIO, UIOv, HSI, ADS methods.
|
|
|
|
the W, Wp, UIO, UIOv, HSI, ADS methods.
|
|
|
|
|
|
|
|
At the end of this section, we construct the test suites for the running example.
|
|
|
|
Our hybrid ADS method uses a similar construction.
|
|
|
|
Our hybrid ADS method uses a similar construction.
|
|
|
|
|
|
|
|
|
|
|
|
There are many more test generation methods.
|
|
|
|
There are many more test generation methods.
|
|
|
|
@ -396,19 +445,26 @@ We fix a state cover $P$ throughout this section and take the transition cover $
|
|
|
|
[title={W-method \cite[DBLP:journals/tse/Chow78, Vasilevskii73]},
|
|
|
|
[title={W-method \cite[DBLP:journals/tse/Chow78, Vasilevskii73]},
|
|
|
|
reference=sec:w]
|
|
|
|
reference=sec:w]
|
|
|
|
|
|
|
|
|
|
|
|
Possibly one of the earliest $m$-complete test methods.
|
|
|
|
After the work of \citet[Moore56], it was unclear whether a test suite of polynomial size could exist.
|
|
|
|
\todo{Opmerking over Moore's vermoeden?}
|
|
|
|
Both \citet[DBLP:journals/tse/Chow78, Vasilevskii73] independently prove that such a test suite exists.
|
|
|
|
|
|
|
|
\footnote{More precisely: the size of $T_{\text{W}}$ is polynomial in the size of the specification for each fixed $k$.}
|
|
|
|
|
|
|
|
The W method is a very structured test suite construction.
|
|
|
|
|
|
|
|
It is called the W method as the characterisation set is often called $W$.
|
|
|
|
|
|
|
|
|
|
|
|
\startdefinition
|
|
|
|
\startdefinition
|
|
|
|
[reference=w-method]
|
|
|
|
[reference=w-method]
|
|
|
|
Let $W$ be a characterisation set, the \defn{W test suite} is
|
|
|
|
Let $W$ be a characterisation set, the \defn{W test suite} is
|
|
|
|
defined as
|
|
|
|
defined as
|
|
|
|
\startformula
|
|
|
|
\startformula
|
|
|
|
(P \cup Q) \cdot I^{\leq k} \cdot W .
|
|
|
|
T_{\text{W}} = (P \cup Q) \cdot I^{\leq k} \cdot W .
|
|
|
|
\stopformula
|
|
|
|
\stopformula
|
|
|
|
\stopdefinition
|
|
|
|
\stopdefinition
|
|
|
|
|
|
|
|
|
|
|
|
\todo{Uitleggen}
|
|
|
|
This -- and all following methods -- tests the machine in two phases.
|
|
|
|
|
|
|
|
For simplicity, we explain these phases when $k = 0$.
|
|
|
|
|
|
|
|
The first phase consists of the tests $P \cdot W$ and tests whether all states of the specification are (roughly) present in the implementation.
|
|
|
|
|
|
|
|
The second phase is $Q \cdot W$ and tests whether the successor states are correct.
|
|
|
|
|
|
|
|
Together, these two phases put enough constraints on the implementation to know that the implementation and specification coincide.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
\stopsubsection
|
|
|
|
\stopsubsection
|
|
|
|
@ -416,15 +472,16 @@ defined as
|
|
|
|
[title={The Wp-method \cite[DBLP:journals/tse/FujiwaraBKAG91]},
|
|
|
|
[title={The Wp-method \cite[DBLP:journals/tse/FujiwaraBKAG91]},
|
|
|
|
reference=sec:wp]
|
|
|
|
reference=sec:wp]
|
|
|
|
|
|
|
|
|
|
|
|
The W-method was refined by Fujiwara et al. to use smaller sets when identifying states.
|
|
|
|
\citet[DBLP:journals/tse/FujiwaraBKAG91] realised that one needs less tests in the second phase of the W method.
|
|
|
|
In order to do that he defined state-local sets of words.
|
|
|
|
Since we already know the right states are present after phase one, we only need to check if the state after a transition is consistent with the expected state.
|
|
|
|
|
|
|
|
This justifies the use of state identifiers for each state.
|
|
|
|
|
|
|
|
|
|
|
|
\startdefinition
|
|
|
|
\startdefinition
|
|
|
|
[reference={state-identifier,wp-method}]
|
|
|
|
[reference={state-identifier,wp-method}]
|
|
|
|
Let $\Fam{W}$ be a family of state identifiers, the \defn{Wp test suite} is
|
|
|
|
Let $\Fam{W}$ be a family of state identifiers, the \defn{Wp test suite} is
|
|
|
|
defined as
|
|
|
|
defined as
|
|
|
|
\startformula
|
|
|
|
\startformula
|
|
|
|
P \cdot I^{\leq k} \cdot \bigcup \Fam{W} \,\cup\, Q \cdot I^{\leq k}
|
|
|
|
T_{\text{Wp}} = P \cdot I^{\leq k} \cdot \bigcup \Fam{W} \,\cup\, Q \cdot I^{\leq k}
|
|
|
|
\odot \Fam{W}.
|
|
|
|
\odot \Fam{W}.
|
|
|
|
\stopformula
|
|
|
|
\stopformula
|
|
|
|
\stopdefinition
|
|
|
|
\stopdefinition
|
|
|
|
@ -439,15 +496,14 @@ Once states are tested as such, we can use the smaller sets $W_s$ for testing tr
|
|
|
|
[title={The HSI-method \cite[LuoPB95, YevtushenkoP90]},
|
|
|
|
[title={The HSI-method \cite[LuoPB95, YevtushenkoP90]},
|
|
|
|
reference=sec:hsi]
|
|
|
|
reference=sec:hsi]
|
|
|
|
|
|
|
|
|
|
|
|
The Wp-method in turn was refined by Yevtushenko and Petrenko.
|
|
|
|
The Wp-method in turn was refined by \citet[LuoPB95, YevtushenkoP90].
|
|
|
|
They make use of so called \emph{harmonised} state identifiers.
|
|
|
|
They make use of so called \emph{harmonised} state identifiers, allowing to take state identifiers in the initial phase of the test suite.
|
|
|
|
By having this global property of the family, less tests need to be executing when testing a state.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
\startdefinition
|
|
|
|
\startdefinition
|
|
|
|
[reference=hsi-method]
|
|
|
|
[reference=hsi-method]
|
|
|
|
Let $\Fam{H}$ be a separating family, the \defn{HSI test suite} is defined as
|
|
|
|
Let $\Fam{H}$ be a separating family, the \defn{HSI test suite} is defined as
|
|
|
|
\startformula
|
|
|
|
\startformula
|
|
|
|
(P \cup Q) \cdot I^{\leq k} \odot \Fam{H}.
|
|
|
|
T_{\text{HSI}} = (P \cup Q) \cdot I^{\leq k} \odot \Fam{H}.
|
|
|
|
\stopformula
|
|
|
|
\stopformula
|
|
|
|
\stopdefinition
|
|
|
|
\stopdefinition
|
|
|
|
|
|
|
|
|
|
|
|
@ -468,7 +524,7 @@ This is exploited in the ADS-method.
|
|
|
|
[reference=ds-method]
|
|
|
|
[reference=ds-method]
|
|
|
|
Let $\Fam{Z}$ be a separating family where every set is a singleton, the \defn{ADS test suite} is defined as
|
|
|
|
Let $\Fam{Z}$ be a separating family where every set is a singleton, the \defn{ADS test suite} is defined as
|
|
|
|
\startformula
|
|
|
|
\startformula
|
|
|
|
(P \cup Q) \cdot I^{\leq k} \odot \Fam{Z}.
|
|
|
|
T_{\text{ADS}} = (P \cup Q) \cdot I^{\leq k} \odot \Fam{Z}.
|
|
|
|
\stopformula
|
|
|
|
\stopformula
|
|
|
|
\stopdefinition
|
|
|
|
\stopdefinition
|
|
|
|
|
|
|
|
|
|
|
|
@ -487,7 +543,7 @@ In a way this is a generalisation of the ADS-method, since the requirement that
|
|
|
|
[reference={uio, uiov-method}]
|
|
|
|
[reference={uio, uiov-method}]
|
|
|
|
Let $\Fam{U} = \{ \text{a single UIO for } s \}_{s \in S}$ be a family of UIO sequences, the \defn{UIOv test suite} is defined as
|
|
|
|
Let $\Fam{U} = \{ \text{a single UIO for } s \}_{s \in S}$ be a family of UIO sequences, the \defn{UIOv test suite} is defined as
|
|
|
|
\startformula
|
|
|
|
\startformula
|
|
|
|
P \cdot I^{\leq k} \cdot \bigcup \Fam{U} \,\cup\, Q \cdot I^{\leq k} \odot \Fam{U}.
|
|
|
|
T_{\text{UIOv}} = P \cdot I^{\leq k} \cdot \bigcup \Fam{U} \,\cup\, Q \cdot I^{\leq k} \odot \Fam{U}.
|
|
|
|
\stopformula
|
|
|
|
\stopformula
|
|
|
|
\stopdefinition
|
|
|
|
\stopdefinition
|
|
|
|
|
|
|
|
|
|
|
|
@ -509,29 +565,29 @@ With the same UIOs as above, the resulting UIOv test suite for the specification
|
|
|
|
[title={An example where the UIO method is not complete.},
|
|
|
|
[title={An example where the UIO method is not complete.},
|
|
|
|
reference=fig:uio-counterexample]
|
|
|
|
reference=fig:uio-counterexample]
|
|
|
|
\startcombination[2*1]
|
|
|
|
\startcombination[2*1]
|
|
|
|
{\hbox{\starttikzpicture
|
|
|
|
{\hbox{\starttikzpicture[node distance=2.5cm, bend angle=18]
|
|
|
|
\node[state,initial,initial text=] (0) {$s_0$};
|
|
|
|
\node[state,initial,initial text=] (0) {$s_0$};
|
|
|
|
\node[state] (1) [above right of=0] {$s_1$};
|
|
|
|
\node[state] (1) [above right of=0] {$s_1$};
|
|
|
|
\node[state] (2) [below right of=1] {$s_2$};
|
|
|
|
\node[state] (2) [below right of=1] {$s_2$};
|
|
|
|
\path[->]
|
|
|
|
\path[->]
|
|
|
|
(0) edge [bend left=20 ] node [left ] {${a}/0$} (1)
|
|
|
|
(0) edge [bend left ] node [left ] {${a}/0$} (1)
|
|
|
|
(0) edge [bend right=15] node [below] {${b}/1$} (2)
|
|
|
|
(0) edge [bend right] node [below] {${b}/1$} (2)
|
|
|
|
(1) edge [bend left=20 ] node [left ] {${a}/1$} (0)
|
|
|
|
(1) edge [bend left ] node [left ] {${a}/1$} (0)
|
|
|
|
(1) edge [bend right=20] node [right] {${b}/1$} (2)
|
|
|
|
(1) edge [bend right] node [right] {${b}/1$} (2)
|
|
|
|
(2) edge [bend right=20] node [below] {${a}/0$} (0)
|
|
|
|
(2) edge [bend right] node [below] {${a}/0$} (0)
|
|
|
|
(2) edge [bend right=15] node [right] {${b}/1$} (1);
|
|
|
|
(2) edge [bend right] node [right] {${b}/1$} (1);
|
|
|
|
\stoptikzpicture}} {Specification}
|
|
|
|
\stoptikzpicture}} {Specification}
|
|
|
|
{\hbox{\starttikzpicture
|
|
|
|
{\hbox{\starttikzpicture[node distance=2.5cm, bend angle=18]
|
|
|
|
\node[state,initial,initial text=] (0) {$s'_0$};
|
|
|
|
\node[state,initial,initial text=] (0) {$s'_0$};
|
|
|
|
\node[state] (1) [above right of=0] {$s'_1$};
|
|
|
|
\node[state] (1) [above right of=0] {$s'_1$};
|
|
|
|
\node[state] (2) [below right of=1] {$s'_2$};
|
|
|
|
\node[state] (2) [below right of=1] {$s'_2$};
|
|
|
|
\path[->]
|
|
|
|
\path[->]
|
|
|
|
(0) edge [bend left=20 ] node [left ] {${a}/0$} (1)
|
|
|
|
(0) edge [bend left ] node [left ] {${a}/0$} (1)
|
|
|
|
(0) edge [bend right=15] node [below] {${b}/1$} (2)
|
|
|
|
(0) edge [bend right] node [below] {${b}/1$} (2)
|
|
|
|
(1) edge [bend left=20 ] node [left ] {${a}/1$} (0)
|
|
|
|
(1) edge [bend left ] node [left ] {${a}/1$} (0)
|
|
|
|
(1) edge [loop ] node [above] {${b}/1$} (1)
|
|
|
|
(1) edge [loop ] node [below] {${b}/1$} (1)
|
|
|
|
(2) edge [bend right=20] node [below] {${a}/0$} (0)
|
|
|
|
(2) edge [bend right] node [below] {${a}/0$} (0)
|
|
|
|
(2) edge [bend right=15] node [right] {${b}/1$} (1);
|
|
|
|
(2) edge [bend right] node [right] {${b}/1$} (1);
|
|
|
|
\stoptikzpicture}} {Implementation}
|
|
|
|
\stoptikzpicture}} {Implementation}
|
|
|
|
\stopcombination
|
|
|
|
\stopcombination
|
|
|
|
\stopplacefigure
|
|
|
|
\stopplacefigure
|
|
|
|
@ -603,7 +659,51 @@ In general, however, UIOs may not exist (and finding them is hard).
|
|
|
|
|
|
|
|
|
|
|
|
The UIO method and ADS method are not applicable in this example because state $s_2$ does not have an UIO.
|
|
|
|
The UIO method and ADS method are not applicable in this example because state $s_2$ does not have an UIO.
|
|
|
|
|
|
|
|
|
|
|
|
\todo{Draaien op faulty implementation}
|
|
|
|
\startplacefigure
|
|
|
|
|
|
|
|
[title={A faulty implementation for the specification in \in{Figure}[fig:running-example].},
|
|
|
|
|
|
|
|
list={A faulty implementation.},
|
|
|
|
|
|
|
|
reference=fig:running-example-faulty]
|
|
|
|
|
|
|
|
\hbox{
|
|
|
|
|
|
|
|
\starttikzpicture[node distance=0.9cm and 3cm,bend angle=20]
|
|
|
|
|
|
|
|
\node[state] (0) {$s'_0$};
|
|
|
|
|
|
|
|
\node[state] (1) [above left = of 0] {$s'_1$};
|
|
|
|
|
|
|
|
\node[state] (2) [below left = of 0] {$s'_2$};
|
|
|
|
|
|
|
|
\node[state] (3) [above right = of 0] {$s'_3$};
|
|
|
|
|
|
|
|
\node[state] (4) [below right = of 0] {$s'_4$};
|
|
|
|
|
|
|
|
\node (5) [above = of 0] {};
|
|
|
|
|
|
|
|
\path[->]
|
|
|
|
|
|
|
|
(5) edge (0)
|
|
|
|
|
|
|
|
(0) edge [bend left] node [below] {$a/1$} (1)
|
|
|
|
|
|
|
|
(0) edge [bend right] node [below] {$b/0$} (4)
|
|
|
|
|
|
|
|
(0) edge [loop below] node [below] {$c/0$} (0)
|
|
|
|
|
|
|
|
(1) edge node [left ] {$a/0$} (2)
|
|
|
|
|
|
|
|
(1) edge [bend left] node [above] {$b/0$, $c/0$} (0)
|
|
|
|
|
|
|
|
(2) edge [bend right] node [below] {$a/1$, $b/0$, $c/0$} (0)
|
|
|
|
|
|
|
|
(3) edge [bend left] node [right] {$a/1$} (4)
|
|
|
|
|
|
|
|
(3) edge [bend right] node [above] {$b/0$} (0)
|
|
|
|
|
|
|
|
(3) edge [loop right] node [right] {$c/1$} (3)
|
|
|
|
|
|
|
|
(4) edge [bend left] node [left ] {$a/1$} (3)
|
|
|
|
|
|
|
|
(4) edge [loop right] node [right] {$b/0$} (4)
|
|
|
|
|
|
|
|
(4) edge [bend right] node [above] {$c/0$} (0);
|
|
|
|
|
|
|
|
\stoptikzpicture
|
|
|
|
|
|
|
|
}
|
|
|
|
|
|
|
|
\stopplacefigure
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
We can run these test suites on the faulty implementation shown in \in{Figure}[fig:running-example-faulty].
|
|
|
|
|
|
|
|
Here, the $a$-transition from state $s'_2$ transitions to the wrong target state.
|
|
|
|
|
|
|
|
It is not an obvious mistake, since the faulty target $s'_0$ has very similar transitions as $s_2$.
|
|
|
|
|
|
|
|
Yet, all the test suites detect this error.
|
|
|
|
|
|
|
|
When choosing the prefix $aaa$ (included in the transition cover), and suffix $aa$ (included in the characterisation set and state identifiers for $s_2$), we see that the specification outputs $10111$ and the implementation outputs $10110$.
|
|
|
|
|
|
|
|
The sequence $aaaaa$ is the only sequence (in any of the test suites here) which detects this fault.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
If on the other hand, the $a$-transition from $s'_2$ would transition to $s'_4$, we need the suffix $ac$ as $aa$ will not detect the fault.
|
|
|
|
|
|
|
|
Since the sequences $ac$ is included in the state identifier for $s_2$, this fault would also be detected.
|
|
|
|
|
|
|
|
This shows that it is sometimes necessary to include multiple sequences in the state identifier.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Another approach to testing would be to enumerate all sequences up to a certain length.
|
|
|
|
|
|
|
|
In this example, we need sequences of at least length 5.
|
|
|
|
|
|
|
|
Consequently, the test suite contains 243 sequences and this boils down to a size of 1458.
|
|
|
|
|
|
|
|
Such a brute-force approach is hence not scalable.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
\stopsubsection
|
|
|
|
\stopsubsection
|
|
|
|
@ -728,7 +828,7 @@ Its $m$-completeness is proven in \in{Section}[sec:completeness].
|
|
|
|
Let $P$ be a state cover, $\Fam{Z'}$ be a family of sets constructed with the Lee and Yannakakis algorithm, and $\Fam{H}$ be a separating family.
|
|
|
|
Let $P$ be a state cover, $\Fam{Z'}$ be a family of sets constructed with the Lee and Yannakakis algorithm, and $\Fam{H}$ be a separating family.
|
|
|
|
The \defn{hybrid ADS} test suite is
|
|
|
|
The \defn{hybrid ADS} test suite is
|
|
|
|
\startformula
|
|
|
|
\startformula
|
|
|
|
T = P \cdot I^{\leq k+1} \odot (\Fam{Z'} ; \Fam{H}).
|
|
|
|
T_{\text{h-ADS}} = P \cdot I^{\leq k+1} \odot (\Fam{Z'} ; \Fam{H}).
|
|
|
|
\stopformula
|
|
|
|
\stopformula
|
|
|
|
\stopdefinition
|
|
|
|
\stopdefinition
|
|
|
|
|
|
|
|
|
|
|
|
@ -741,9 +841,9 @@ We note that the states $s_2, s_3, s_4$ are not split, so we need to refine the
|
|
|
|
|
|
|
|
|
|
|
|
\startplacefigure
|
|
|
|
\startplacefigure
|
|
|
|
[title={(a): Largest splitting tree with only valid splits for \in{Figure}[fig:running-example].
|
|
|
|
[title={(a): Largest splitting tree with only valid splits for \in{Figure}[fig:running-example].
|
|
|
|
(b): Its adaptive distinguishing tree in notation of \citet[DBLP:journals/tc/LeeY94].},
|
|
|
|
(b): Its incomplete adaptive distinguishing tree.},
|
|
|
|
list={Splitting tree and adaptive distinguishing sequence.},
|
|
|
|
list={Splitting tree and incomplete adaptive distinguishing sequence.},
|
|
|
|
reference=fig:example-splitting-tree]
|
|
|
|
reference=fig:example-ads]
|
|
|
|
\startcombination[2*1]{
|
|
|
|
\startcombination[2*1]{
|
|
|
|
\hbox{
|
|
|
|
\hbox{
|
|
|
|
\starttikzpicture[node distance=2cm]
|
|
|
|
\starttikzpicture[node distance=2cm]
|
|
|
|
@ -760,26 +860,27 @@ We note that the states $s_2, s_3, s_4$ are not split, so we need to refine the
|
|
|
|
\stoptikzpicture
|
|
|
|
\stoptikzpicture
|
|
|
|
}} {(a)}
|
|
|
|
}} {(a)}
|
|
|
|
{\hbox{
|
|
|
|
{\hbox{
|
|
|
|
\starttikzpicture[node distance=2cm]
|
|
|
|
\starttikzpicture[node distance=.75cm]
|
|
|
|
\adsnode{0}{s_0, s_1, s_2, s_3, s_4}{s_0, s_1, s_2, s_3, s_4}{a}{}
|
|
|
|
\node (0) {$a$};
|
|
|
|
\adsnode{1}{s_1}{s_2}{}{below left of=0}
|
|
|
|
\node [below left =of 0] (1) {$s_1$};
|
|
|
|
\adsnode{2}{s_0, s_2, s_3, s_4}{s_1, s_2, s_4, s_3}{aa}{below right of=0}
|
|
|
|
\node [below right=of 0] (2) {$a$};
|
|
|
|
\adsnode{3}{s_0}{s_2}{}{below left of=2}
|
|
|
|
\node [below left =of 2] (3) {$s_0$};
|
|
|
|
\adsnode{4}{s_2, s_3, s_4}{s_2, s_3, s_4}{}{below right of=2}
|
|
|
|
\node [below right=of 2] (4) {$s_2, s_3, s_4$};
|
|
|
|
\path[->]
|
|
|
|
|
|
|
|
(0) edge (1)
|
|
|
|
\path[->]
|
|
|
|
(0) edge (2)
|
|
|
|
(0)+(0,.75) edge (0)
|
|
|
|
(2) edge (3)
|
|
|
|
(0) edge node [above left ] {$0$} (1)
|
|
|
|
(2) edge (4);
|
|
|
|
(0) edge node [above right] {$1$} (2)
|
|
|
|
|
|
|
|
(2) edge node [above left ] {$0$} (3)
|
|
|
|
|
|
|
|
(2) edge node [above right] {$1$} (4);
|
|
|
|
\stoptikzpicture
|
|
|
|
\stoptikzpicture
|
|
|
|
}} {(b)}
|
|
|
|
}} {(b)}
|
|
|
|
\stopcombination
|
|
|
|
\stopcombination
|
|
|
|
\stopplacefigure
|
|
|
|
\stopplacefigure
|
|
|
|
|
|
|
|
|
|
|
|
\todo{Dit eerder noemen. En zeggen: we take the same $\Fam{H}$ as before.}
|
|
|
|
We take the separating family $\Fam{H}$ from before.
|
|
|
|
From the splitting tree in \in{Figure}[fig:example-splitting-tree], we obtain the following separating family $\Fam{H}$.
|
|
|
|
From the incomplete ADS in \in{Figure}{b}[fig:example-ads] above we obtain the family $\Fam{Z'}$.
|
|
|
|
From the figure above we obtain the family $\Fam{Z'}$.
|
|
|
|
These families and the refinement $\Fam{Z'}; \Fam{H}$ are given below.
|
|
|
|
These families and the refinement $\Fam{Z'}; \Fam{H}$ are given below:
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
\startformula\startmathmatrix[n=3,align={left,left,left},distance=1cm]
|
|
|
|
\startformula\startmathmatrix[n=3,align={left,left,left},distance=1cm]
|
|
|
|
\NC H_0 = \{aa,c\} \NC Z'_0 = \{aa\} \NC (Z';H)_0 = \{aa\} \NR
|
|
|
|
\NC H_0 = \{aa,c\} \NC Z'_0 = \{aa\} \NC (Z';H)_0 = \{aa\} \NR
|
|
|
|
@ -817,6 +918,14 @@ A trie data structure also allows us to immediately obtain the set of maximal te
|
|
|
|
\startsubsection
|
|
|
|
\startsubsection
|
|
|
|
[title={Randomisation}]
|
|
|
|
[title={Randomisation}]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Many constructions of the test suite generation can be randomised.
|
|
|
|
|
|
|
|
There may exist many shortest access sequences to a state and we can randomly pick any.
|
|
|
|
|
|
|
|
Also in the construction of state identifiers many steps in the algorithm are non-deterministic:
|
|
|
|
|
|
|
|
the algorithm may ask to find any input symbol which separates a set of states.
|
|
|
|
|
|
|
|
The tool randomises many such choices.
|
|
|
|
|
|
|
|
We have noticed that this can have a huge influence on the size of the test suite.
|
|
|
|
|
|
|
|
However, a decent statistical investigation still lacks at the moment.
|
|
|
|
|
|
|
|
|
|
|
|
In many of the applications such as learning, no bound on the number of states of the SUT was known.
|
|
|
|
In many of the applications such as learning, no bound on the number of states of the SUT was known.
|
|
|
|
In such cases it is possible to randomly select test cases from an infinite test suite.
|
|
|
|
In such cases it is possible to randomly select test cases from an infinite test suite.
|
|
|
|
Unfortunately, we lose the theoretical guarantees of completeness with random generation.
|
|
|
|
Unfortunately, we lose the theoretical guarantees of completeness with random generation.
|
|
|
|
@ -848,6 +957,7 @@ We classify them in two directions,
|
|
|
|
[reference=thm:completeness]
|
|
|
|
[reference=thm:completeness]
|
|
|
|
The following test suites are all $n+k$-complete:
|
|
|
|
The following test suites are all $n+k$-complete:
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
\placetable[force,none]{}{
|
|
|
|
\starttabulate[|c|c|c|]
|
|
|
|
\starttabulate[|c|c|c|]
|
|
|
|
\NC \NC Arbitrary \NC Harmonised
|
|
|
|
\NC \NC Arbitrary \NC Harmonised
|
|
|
|
\NR \HL %----------------------------------------
|
|
|
|
\NR \HL %----------------------------------------
|
|
|
|
@ -869,11 +979,9 @@ The following test suites are all $n+k$-complete:
|
|
|
|
\NC $ P \cdot I^{\leq k} \cdot \bigcup \Fam{U} \,\cup\, Q \cdot I^{\leq k} \odot \Fam{U} $
|
|
|
|
\NC $ P \cdot I^{\leq k} \cdot \bigcup \Fam{U} \,\cup\, Q \cdot I^{\leq k} \odot \Fam{U} $
|
|
|
|
\NC $ (P \cup Q) \cdot I^{\leq k} \odot \Fam{Z} $
|
|
|
|
\NC $ (P \cup Q) \cdot I^{\leq k} \odot \Fam{Z} $
|
|
|
|
\NR \HL %----------------------------------------
|
|
|
|
\NR \HL %----------------------------------------
|
|
|
|
\stoptabulate
|
|
|
|
\stoptabulate}
|
|
|
|
\stoptheorem
|
|
|
|
\stoptheorem
|
|
|
|
|
|
|
|
|
|
|
|
\todo{Iets zeggen over de hybrid UIO method?}
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
It should be noted that the ADS-method is a specific instance of the HSI-method and similarly the UIOv-method is an instance of the Wp-method.
|
|
|
|
It should be noted that the ADS-method is a specific instance of the HSI-method and similarly the UIOv-method is an instance of the Wp-method.
|
|
|
|
What is generally meant by the Wp-method and HSI-method is the above formula together with a particular way to obtain the (harmonised) state identifiers.
|
|
|
|
What is generally meant by the Wp-method and HSI-method is the above formula together with a particular way to obtain the (harmonised) state identifiers.
|
|
|
|
|
|
|
|
|
|
|
|
@ -894,21 +1002,36 @@ For the W, Wp, HSI and hybrid ADS methods we obtained test suites of size 169, 7
|
|
|
|
[title={Proof of completeness},
|
|
|
|
[title={Proof of completeness},
|
|
|
|
reference=sec:completeness]
|
|
|
|
reference=sec:completeness]
|
|
|
|
|
|
|
|
|
|
|
|
\todo{Stukje over bisimulaties?}
|
|
|
|
In this section, we will proof $n$-completeness of the discussed test methods.
|
|
|
|
|
|
|
|
|
|
|
|
We fix a specification $M$ which has a minimal representative with $n$ states and an implementation $M'$ with at most $n+k$ states.
|
|
|
|
We fix a specification $M$ which has a minimal representative with $n$ states and an implementation $M'$ with at most $n+k$ states.
|
|
|
|
We assume that all states are reachable from the initial state in both machines (i.e., both are \defn{connected}).
|
|
|
|
We assume that all states are reachable from the initial state in both machines (i.e., both are \defn{connected}).
|
|
|
|
We define the following notation:
|
|
|
|
|
|
|
|
|
|
|
|
Before we dive into the proof, we give some background on the proof-principle of bisimulation.
|
|
|
|
|
|
|
|
The original proofs of completeness often involve an inductive argument (on the length of words) inlined with arguments about characterisation sets.
|
|
|
|
|
|
|
|
This can be hard to follow and so we prefer a proof based on bisimulations, which defers the inductive argument to a general statement about bisimulation.
|
|
|
|
|
|
|
|
Many notions of bisimulation exist in the theory of labelled transition systems, but for Mealy machines there is just one simple definition.
|
|
|
|
|
|
|
|
We give the definition and the main proof principle, all of which can be found in \citep[Rutten98].
|
|
|
|
|
|
|
|
|
|
|
|
\startdefinition
|
|
|
|
\startdefinition
|
|
|
|
Let $W \subseteq I^{\ast}$ be a set of words.
|
|
|
|
Let $M$ be a Mealy machine.
|
|
|
|
Two states $x, y$ (of possibly different machines) are $W$-equivalent, written $x \sim_W y$, if $\lambda(x, w) = \lambda(y, w)$ for all $w \in W$.
|
|
|
|
A relation $R \subseteq S \times S$ is called a \defn{bisimulation} if for every $(s, t) \in R$ we have
|
|
|
|
|
|
|
|
\startitemize
|
|
|
|
|
|
|
|
\item equal outputs: $\lambda(s, a) = \lambda(t, a)$ for all $a \in I$, and
|
|
|
|
|
|
|
|
\item related successor states: $(\delta(s, a), \delta(t, a)) \in R$ for all $a \in I$.
|
|
|
|
|
|
|
|
\stopitemize
|
|
|
|
\stopdefinition
|
|
|
|
\stopdefinition
|
|
|
|
|
|
|
|
|
|
|
|
We note that for a fixed set $W$ the relation $\sim_W$ is a equivalence relation and that $W \subseteq V$ gives $x \sim_V y \implies x \sim_W y$.
|
|
|
|
\startlemma
|
|
|
|
The next lemma gives sufficient conditions for a test suite of the given anatomy to be
|
|
|
|
If two states $s, t$ are related by a bisimulation $R$, then $s \sim t$.
|
|
|
|
|
|
|
|
\stoplemma
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
In the following proof, we use a slight generalisation of the bisimulation proof technique, callend \emph{bisimulation up-to}.
|
|
|
|
|
|
|
|
This allows one to give a smaller set $R$ which extends to a bisimulation.
|
|
|
|
|
|
|
|
A good introduction of these up-to techniques is given by \citet[DBLP:journals/cacm/BonchiP15] or the thesis of \citet[Rot17].
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
The next proposition gives sufficient conditions for a test suite of a certain shape to be
|
|
|
|
complete.
|
|
|
|
complete.
|
|
|
|
We then prove that these conditions hold for the test suites in this paper.
|
|
|
|
We then prove that these conditions hold for the test suites in this chapter.
|
|
|
|
|
|
|
|
|
|
|
|
\startproposition
|
|
|
|
\startproposition
|
|
|
|
[reference=prop:completeness]
|
|
|
|
[reference=prop:completeness]
|
|
|
|
@ -921,7 +1044,6 @@ If
|
|
|
|
\item the machines $M$ and $M'$ agree on $T$,
|
|
|
|
\item the machines $M$ and $M'$ agree on $T$,
|
|
|
|
\stopitemize
|
|
|
|
\stopitemize
|
|
|
|
then $M$ and $M'$ are equivalent.
|
|
|
|
then $M$ and $M'$ are equivalent.
|
|
|
|
\todo{Puntje 2 verdient meer aandacht?}
|
|
|
|
|
|
|
|
\stopproposition
|
|
|
|
\stopproposition
|
|
|
|
\startproof
|
|
|
|
\startproof
|
|
|
|
First, we prove that $P \cdot I^{\leq k}$ reaches all states in $M'$.
|
|
|
|
First, we prove that $P \cdot I^{\leq k}$ reaches all states in $M'$.
|
|
|
|
@ -932,7 +1054,7 @@ Now $n$ states are reached by the previous argument (using the set $P$).
|
|
|
|
By assumption $M'$ has at most $k$ extra states and so we can reach all those extra states by using $I^{\leq k}$ after $P$.
|
|
|
|
By assumption $M'$ has at most $k$ extra states and so we can reach all those extra states by using $I^{\leq k}$ after $P$.
|
|
|
|
|
|
|
|
|
|
|
|
Second, we show that the reached states are bisimilar.
|
|
|
|
Second, we show that the reached states are bisimilar.
|
|
|
|
Define the relation $R = \{(\delta(q_0, p), \delta'(q_0', p)) \mid p \in P \cdot I^{\leq k}\}$.
|
|
|
|
Define the relation $R = \{(\delta(s_0, p), \delta'(s_0', p)) \mid p \in P \cdot I^{\leq k}\}$.
|
|
|
|
Note that for each $(s, i) \in R$ we have $s \sim_{W_s} i$.
|
|
|
|
Note that for each $(s, i) \in R$ we have $s \sim_{W_s} i$.
|
|
|
|
For each state $i \in M'$ there is a state $s \in M$ such that $(s, i) \in R$, since we reach all states in both machines by $P \cdot I^{\leq k}$.
|
|
|
|
For each state $i \in M'$ there is a state $s \in M$ such that $(s, i) \in R$, since we reach all states in both machines by $P \cdot I^{\leq k}$.
|
|
|
|
We will prove that this relation is in fact a bisimulation up-to equivalence.
|
|
|
|
We will prove that this relation is in fact a bisimulation up-to equivalence.
|
|
|
|
@ -947,12 +1069,11 @@ So we have:
|
|
|
|
By the second assumption, we conclude that $s_2 \sim t$.
|
|
|
|
By the second assumption, we conclude that $s_2 \sim t$.
|
|
|
|
So $s_2 \sim t$ and $(t, i) \in R$, which means that $R$ is a bisimulation up-to equivalence.
|
|
|
|
So $s_2 \sim t$ and $(t, i) \in R$, which means that $R$ is a bisimulation up-to equivalence.
|
|
|
|
Using the theory of up-to techniques \cite[DBLP:journals/cacm/BonchiP15] we know that there exists a bisimulation relation containing $R$.
|
|
|
|
Using the theory of up-to techniques \cite[DBLP:journals/cacm/BonchiP15] we know that there exists a bisimulation relation containing $R$.
|
|
|
|
\todo{Up to is best nieuw. Misschien meer aandacht aan besteden. Ook nog Jurriaan citeren?}
|
|
|
|
In particular, the initial $s_0$ and $s'_0$ are bisimilar.
|
|
|
|
In particular $q_0$ and $q'_0$ are bisimilar.
|
|
|
|
|
|
|
|
And so the machines $M$ and $M'$ are equivalent.
|
|
|
|
And so the machines $M$ and $M'$ are equivalent.
|
|
|
|
\stopproof
|
|
|
|
\stopproof
|
|
|
|
|
|
|
|
|
|
|
|
Before we show that the conditions hold for the test methods described in this paper, we reflect on the above proof first.
|
|
|
|
Before we show that the conditions hold for the test methods, we reflect on the above proof first.
|
|
|
|
This proof is very similar to the completeness proof by \citet[DBLP:journals/tse/Chow78].
|
|
|
|
This proof is very similar to the completeness proof by \citet[DBLP:journals/tse/Chow78].
|
|
|
|
(In fact, it is also similar to Lemma 4 by \citet[DBLP:journals/iandc/Angluin87] which proves termination in the L* learning algorithm. This correspondence was noted by \citet[DBLP:conf/fase/BergGJLRS05].)
|
|
|
|
(In fact, it is also similar to Lemma 4 by \citet[DBLP:journals/iandc/Angluin87] which proves termination in the L* learning algorithm. This correspondence was noted by \citet[DBLP:conf/fase/BergGJLRS05].)
|
|
|
|
In the first part we argue that all states are visited by using some sort of counting and reachability argument.
|
|
|
|
In the first part we argue that all states are visited by using some sort of counting and reachability argument.
|
|
|
|
@ -994,7 +1115,8 @@ The HSI, ADS and hybrid ADS test suites are $n+k$-complete.
|
|
|
|
|
|
|
|
|
|
|
|
\stopsection
|
|
|
|
\stopsection
|
|
|
|
\startsection
|
|
|
|
\startsection
|
|
|
|
[title={Related Work and Discussion}]
|
|
|
|
[title={Related Work and Discussion},
|
|
|
|
|
|
|
|
reference=sec:discussion]
|
|
|
|
|
|
|
|
|
|
|
|
\todo{Veel gerelateerd werk kan naar de grote intro.}
|
|
|
|
\todo{Veel gerelateerd werk kan naar de grote intro.}
|
|
|
|
|
|
|
|
|
|
|
|
@ -1006,8 +1128,8 @@ It does not generalise to extra states, but it seems to construct very small tes
|
|
|
|
The H method is a refinement of the HSI method where state identifiers for a testing transitions are reconsidered.
|
|
|
|
The H method is a refinement of the HSI method where state identifiers for a testing transitions are reconsidered.
|
|
|
|
(Note that \in{Proposition}[prop:completeness] allows for a different family when testing transitions.)
|
|
|
|
(Note that \in{Proposition}[prop:completeness] allows for a different family when testing transitions.)
|
|
|
|
Last, the SPY method builds upon the HSI-method and changes the prefixes in order to minimise the size of a test suite, exploiting overlap in test sequences.
|
|
|
|
Last, the SPY method builds upon the HSI-method and changes the prefixes in order to minimise the size of a test suite, exploiting overlap in test sequences.
|
|
|
|
We believe that this technique is independent of the HSI-method and can in fact be applied to all methods presented in this paper.
|
|
|
|
We believe that this technique is independent of the HSI-method and can in fact be applied to all methods presented in this chapter.
|
|
|
|
As such, the SPY method should be considered as an optimisation technique, orthogonal to the work in this paper.
|
|
|
|
As such, the SPY method should be considered as an optimisation technique, orthogonal to the work in this chapter.
|
|
|
|
|
|
|
|
|
|
|
|
Recently, \citet[DBLP:journals/cj/HieronsT15] devise a novel test method which is based on incomplete distinguishing sequences and is similar to the hybrid ADS method.
|
|
|
|
Recently, \citet[DBLP:journals/cj/HieronsT15] devise a novel test method which is based on incomplete distinguishing sequences and is similar to the hybrid ADS method.
|
|
|
|
They use sequences which can be considered to be adaptive distinguishing sequences on a subset of the state space.
|
|
|
|
They use sequences which can be considered to be adaptive distinguishing sequences on a subset of the state space.
|
|
|
|
|
Joshua Moerman