joshua/phd-thesis
Archived
1
Fork 0
Code Activity

Meer over test methodes

Browse source
This commit is contained in:
Joshua Moerman 2018-11-03 14:53:05 +01:00
parent 024d290b66
commit cdeaf3321a
2 changed files with 208 additions and 100 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

293
content/test-methods.tex
View file

@ -46,6 +46,8 @@ The \emph{behaviour} of a state $s$ is given by the output function $\lambda(s,
Two states $s$ and $t$ are \emph{equivalent} if they have equal behaviours, written $s \sim t$, and two Mealy machines are equivalent if their initial states are equivalent. Two states $s$ and $t$ are \emph{equivalent} if they have equal behaviours, written $s \sim t$, and two Mealy machines are equivalent if their initial states are equivalent.
\stopdefinition \stopdefinition
\todo{Conventie: $x$ hoort bij een unieke $M$.}
An example Mealy machine is given in \in{Figure}[fig:running-example]. An example Mealy machine is given in \in{Figure}[fig:running-example].
We note that a Mealy machine is deterministic and complete by definition. We note that a Mealy machine is deterministic and complete by definition.
This means that for each state $s$ and each word $w$, there is a unique state $t$ by running the word $w$ from $s$. This means that for each state $s$ and each word $w$, there is a unique state $t$ by running the word $w$ from $s$.
@ -101,12 +103,11 @@ We are able to reset the system, i.e., bring it back to the initial state.
\startdefinition[reference=test-suite] \startdefinition[reference=test-suite]
A \emph{test suite} is a finite subset $T \subseteq I^{\ast}$. A \emph{test suite} is a finite subset $T \subseteq I^{\ast}$.
\stopdefinition
A test $t \in T$ is called \emph{maximal} if it is not a proper prefix of another $s \in T$. A test $t \in T$ is called \emph{maximal} if it is not a proper prefix of another $s \in T$.
We denote the set of maximal tests of $T$ with $max(T)$. We denote the set of maximal tests of $T$ with $max(T)$.
\todo{In de voorbeelden geef ik altijd $max(X)$, \todo{Conventie: Alles is prefix closed. Behalve in de voorbeelden en implementatie.}
maar in de bewijzen is juist $Pref(X)$ handig.
Moet dit consistent houden...}
\stopdefinition
The maximal tests are the only tests in $T$ we actually have to apply to our SUT as we can record the intermediate outputs. The maximal tests are the only tests in $T$ we actually have to apply to our SUT as we can record the intermediate outputs.
Also note that we do not have to encode outputs in the test suite, as those follow from the deterministic specification. Also note that we do not have to encode outputs in the test suite, as those follow from the deterministic specification.
@ -212,6 +213,7 @@ For instance, the set $\{aa, ac, c\}$ will separate $s_2$ from all other states.
As the example shows, we need sets of sequences and sometimes even sets of sets of sqeuences -- called \emph{families}. As the example shows, we need sets of sequences and sometimes even sets of sets of sqeuences -- called \emph{families}.
\footnote{A family of often written as $\{X_s\}_{s \in M}$ or simply $\{X_s\}_{s}$, meaning that for each state $s \in M$ we have a set $X_s$.} \footnote{A family of often written as $\{X_s\}_{s \in M}$ or simply $\{X_s\}_{s}$, meaning that for each state $s \in M$ we have a set $X_s$.}
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.
\todo{Alles eindig?}
\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. \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.
\item A \defn{state identifier} for a state $s$ is a set $W$ which contains a separating sequence for every other state $t$. \item A \defn{state identifier} for a state $s$ is a set $W$ which contains a separating sequence for every other state $t$.
@ -227,7 +229,7 @@ An ads is of special interest since they can identify a state using a single wor
These notions are again related. These notions are again related.
We obtain a characterisation set by taking the union of state identifiers for each state. We obtain a characterisation set by taking the union of state identifiers for each state.
For every machine we can construct a set of harmonised state identifiers as will be shown in \in{Chapter}[chap:separating-sequences] and hence every machine has a characterisation set. For every machine we can construct a set of harmonised state identifiers as will be shown in \in{Chapter}[chap:separating-sequences] and hence every machine has a characterisation set.
However, an adaptive distinguishing sequence may not exist. However, an adaptive distinguishing sequence may not exist, even if every state has an UIO.
\startexample \startexample
As mentioned before, state $s_2$ from \in{Figure}[fig:running-example] has a state identifier $\{aa, ac, b\}$. As mentioned before, state $s_2$ from \in{Figure}[fig:running-example] has a state identifier $\{aa, ac, b\}$.
@ -252,6 +254,7 @@ If $P$ is a state cover, $P \cdot I$ is called a \emph{transition cover}.
In order to define a test suite modularly, we introduce notation for combining sets of words. In order to define a test suite modularly, we introduce notation for combining sets of words.
For sets of words $X$ and $Y$, we define: For sets of words $X$ and $Y$, we define:
\todo{Nog eens herhalen dat het prefix closed is?}
\startitemize[after] \startitemize[after]
\item their concatenation $X \cdot Y = \{ xy \mid x \in X, y \in Y \}$, \item their concatenation $X \cdot Y = \{ xy \mid x \in X, y \in Y \}$,
@ -291,6 +294,9 @@ For all families $\Fam{X}$ and $\Fam{Y}$:
\item $\Fam{X} ; \Fam{Y}$ is a separating family whenever $\Fam{Y}$ is a separating family. \item $\Fam{X} ; \Fam{Y}$ is a separating family whenever $\Fam{Y}$ is a separating family.
\stopitemize \stopitemize
\stoplemma \stoplemma
\startproof
\todo{Kort uitschrijven}
\stopproof
\stopsubsection \stopsubsection
@ -307,8 +313,8 @@ There are many more test generation methods.
Literature shows, however, that not all of them are complete. Literature shows, however, that not all of them are complete.
For example, the method by \citet[DBLP:journals/tosem/Bernhard94] are falsified by \citet[DBLP:journals/tosem/Petrenko97] and the UIO-method from \citet[DBLP:journals/cn/SabnaniD88] is shown to be incomplete by \citet[DBLP:conf/sigcomm/ChanVO89]. For example, the method by \citet[DBLP:journals/tosem/Bernhard94] are falsified by \citet[DBLP:journals/tosem/Petrenko97] and the UIO-method from \citet[DBLP:journals/cn/SabnaniD88] is shown to be incomplete by \citet[DBLP:conf/sigcomm/ChanVO89].
For that reason, completeness of the correct methods is shown in the next section. For that reason, completeness of the correct methods is shown in the next section.
The proof is general enough to capture all the methods at once.
We fix a state cover $P$ throughout this section and take the transition cover $Q = P \cdot I$. We fix a state cover $P$ throughout this section and take the transition cover $Q = P \cdot I$.
\todo{In v1 gebruik ik een andere volgorde: UIOv, Wp, HSI, ADS. Ook voorbeeld uitrekenen.}
\startsubsection \startsubsection
@ -327,20 +333,25 @@ defined as
\stopformula \stopformula
\stopdefinition \stopdefinition
\todo{Uitleggen}
\stopsubsection \stopsubsection
\startsubsection \startsubsection
[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 to use smaller sets when identifying states. The W-method was refined by Fujiwara et al. to use smaller sets when identifying states.
In order to do that he defined state-local sets of words. In order to do that he defined state-local sets of words.
\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 $P \cdot I^{\leq k} \cdot \bigcup \Fam{W} \,\cup\, Q \cdot I^{\leq k} defined as
\odot \Fam{W}$. \startformula
P \cdot I^{\leq k} \cdot \bigcup \Fam{W} \,\cup\, Q \cdot I^{\leq k}
\odot \Fam{W}.
\stopformula
\stopdefinition \stopdefinition
Note that $\bigcup \Fam{W}$ is a characterisation set as defined for the W-method. Note that $\bigcup \Fam{W}$ is a characterisation set as defined for the W-method.
@ -354,17 +365,19 @@ Once states are tested as such, we can use the smaller sets $W_s$ for testing tr
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 Yevtushenko and Petrenko.
They make use of so called \emph{harmonised} state identifiers (which are called separating families in \cite[DBLP:journals/tc/LeeY94] and in present paper). They make use of so called \emph{harmonised} state identifiers.
By having this global property of the family, less tests need to be executing when testing a state. 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
$(P \cup Q) \cdot I^{\leq k} \odot \Fam{H}$. \startformula
(P \cup Q) \cdot I^{\leq k} \odot \Fam{H}.
\stopformula
\stopdefinition \stopdefinition
Our newly described test method is an instance of the HSI-method. Our newly described test method is an instance of the HSI-method.
However, in \cite[LuoPB95, YevtushenkoP90] they describe the HSI-method together with a specific way of generating the separating families. However, \citet[LuoPB95, YevtushenkoP90] describe the HSI-method together with a specific way of generating the separating families.
Namely, the set obtained by a splitting tree with shortest witnesses. Namely, the set obtained by a splitting tree with shortest witnesses.
In present paper that is generalised, allowing for our extension to be an instance. In present paper that is generalised, allowing for our extension to be an instance.
@ -380,7 +393,9 @@ This is exploited in the ADS-method.
\startdefinition \startdefinition
[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
$(P \cup Q) \cdot I^{\leq k} \odot \Fam{Z}$. \startformula
(P \cup Q) \cdot I^{\leq k} \odot \Fam{Z}.
\stopformula
\stopdefinition \stopdefinition
@ -397,12 +412,14 @@ In a way this is a generalisation of the ADS-method, since the requirement that
\startdefinition \startdefinition
[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
$P \cdot I^{\leq k} \cdot \bigcup \Fam{U} \,\cup\, Q \cdot I^{\leq k} \odot \Fam{U}$. \startformula
P \cdot I^{\leq k} \cdot \bigcup \Fam{U} \,\cup\, Q \cdot I^{\leq k} \odot \Fam{U}.
\stopformula
\stopdefinition \stopdefinition
One might think that using a single UIO sequence instead of the set $\bigcup \Fam{U}$ to verify the state is enough. One might think that using a single UIO sequence instead of the set $\bigcup \Fam{U}$ to verify the state is enough.
In fact, this idea was used for the UIO-method which defines the test suite $(P \cup Q) \cdot I^{\leq k} \odot \Fam{U}$. In fact, this idea was used for the UIO-method which defines the test suite $(P \cup Q) \cdot I^{\leq k} \odot \Fam{U}$.
The example in \in{Figure}[fig:uio-counterexample] shows that this does not necessarily define a 3-complete test suite (this example is due to \citenp[DBLP:conf/sigcomm/ChanVO89]). The example in \in{Figure}[fig:uio-counterexample] shows that this does not necessarily define a 3-complete test suite. (This example is due to \citenp[DBLP:conf/sigcomm/ChanVO89]).
Take for example the UIOs $u_0 = aa, u_1 = a, u_2 = ba$ for the states $s_0, s_1, s_2$ respectively. Take for example the UIOs $u_0 = aa, u_1 = a, u_2 = ba$ for the states $s_0, s_1, s_2$ respectively.
The test suite then becomes $\{ aaaa, abba, baaa, bba \}$ and the faulty implementation passes this suite. The test suite then becomes $\{ aaaa, abba, baaa, bba \}$ and the faulty implementation passes this suite.
This happens because the sequence $u_2$ is not an UIO in the implementation, and the state $s'_2$ simulates both UIOs $u_1$ and $u_2$. This happens because the sequence $u_2$ is not an UIO in the implementation, and the state $s'_2$ simulates both UIOs $u_1$ and $u_2$.
@ -443,21 +460,89 @@ With the same UIOs as above, the resulting UIOv test suite for the specification
\stopsubsection \stopsubsection
\startsubsection \startsubsection
[title={Example},
reference=sec:all-example]
Let us compute all the previous test suites on the specification in \in{Figure}[fig:running-example].
We will be testing without extra states, i.e., we construct 5-complete test suites.
We start by defining the state and transition cover.
For this, we simply take all shortest sequences from the initial state to the other states:
\startformula\startalign
\NC P \NC = \{ \epsilon, a, aa, b, ba \} \NR
\NC Q = P \cdot I \NC = \{ a, b, c, aa, ab, ac, aaa, aab, aac, ba, bb, bc, baa, bab, bac \} \NR
\stopalign\stopformula
As shown earlier, the set $W = \{ aa, ac, c \}$ is a characterisation set.
The the W-method gives the following test suite of size 169:
\setupformulas[split=yes,hang=auto]
\startformula
T_{\text{W}} = \{ \alignhere aaaaa, aaaac, aaac, aabaa, aabac, aabc, aacaa, \breakhere
aacac, aacc, abaa, abac, abc, acaa, acac, acc, baaaa, \breakhere
baaac, baac, babaa, babac, babc, bacaa, bacac, bacc, \breakhere
bbaa, bbac, bbc, bcaa, bcac, bcc, caa, cac, cc \} \breakhere
\stopformula
With the Wp-method we get to choose a different state identifier per state.
Since many states have an UIO, we can use them as state identifiers.
This defines the following family $\Fam{W}$:
\startformulas
\startformula W_0 = \{ aa \} \stopformula
\startformula W_1 = \{ a \} \stopformula
\startformula W_2 = \{ aa, ac, c \} \stopformula
\startformula W_3 = \{ c \} \stopformula
\startformula W_4 = \{ ac \} \stopformula
\stopformulas
For the first part of the Wp test suite we need $\bigcup \Fam{W} = \{ aa, ac, c \}$.
For the second part, we only combine the sequences in the transition cover with the corresponding suffixes.
All in al we get a test suite of size 75:
\startformula
T_{\text{Wp}} = \{ \alignhere aaaaa, aaaac, aaac, aabaa, aacaa, abaa, acaa, \breakhere
baaac, baac, babaa, bacc, bbac, bcaa, caa \} \breakhere
\stopformula
For the HSI method we need a separating family.
We pick the following sets:
\startformulas
\startformula H_0 = \{ aa, c \} \stopformula
\startformula H_1 = \{ a \} \stopformula
\startformula H_2 = \{ aa, ac, c \} \stopformula
\startformula H_3 = \{ a, c \} \stopformula
\startformula H_4 = \{ aa, ac, c \} \stopformula
\stopformulas
Note that these sets are harmonised, unlike the family $\Fam{W}$.
For example, the separating sequence $a$ is contained in both $H_1$ and $H_3$.
This ensures that we do not have to consider $\bigcup \Fam{H}$ in the first part of the test suite.
When combining this with the corresponding prefixes, we obtain the HSI test suite of size 125:
\startformula
T_{\text{HSI}} = \{ \alignhere aaaaa, aaaac, aaac, aabaa, aabc, aacaa, \breakhere
aacc, abaa, abc, acaa, acc, baaaa, baaac, baac, babaa, \breakhere
babc, baca, bacc, bbaa, bbac, bbc, bcaa, bcc, caa, cc \} \breakhere
\stopformula
On this particular example the Wp method outperforms the HSI method.
The reason is that many states have UIOs and we picked those to be the state identifiers.
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.
\stopsubsection
\stopsection
\startsection
[title={Hybrid ADS method}, [title={Hybrid ADS method},
reference=sec:hybrid] reference=sec:hybrid]
\todo{Referentie naar volgend hoofdstuk over Oce}
In this section we describe a new test generation method for Mealy machines. In this section we describe a new test generation method for Mealy machines.
Its completeness will be proven in a later section, together with completeness for all methods defined in this section. Its completeness will be proven in a later section, together with completeness for all methods defined in this section.
From a high level perspective, the method uses the algorithm by \cite[authoryears][DBLP:journals/tc/LeeY94] to obtain an ads. From a high level perspective, the method uses the algorithm by \cite[authoryears][DBLP:journals/tc/LeeY94] to obtain an ADS.
If no ads exists, their algorithm still provides some sequences which separates some inequivalent states. If no ADS exists, their algorithm still provides some sequences which separates some inequivalent states.
Our extension is to refine the set of sequences by using pairwise separating sequences. Our extension is to refine the set of sequences by using pairwise separating sequences.
Hence, this method is a hybrid between the ADS-method and HSI-method. Hence, this method is a hybrid between the ADS-method and HSI-method.
The reason we do this is the fact that the ADS-method generally constructs small test suites as experiments by \cite[authoryears][DBLP:journals/infsof/DorofeevaEMCY10] suggest. The reason we do this is the fact that the ADS-method generally constructs small test suites as experiments by \cite[authoryears][DBLP:journals/infsof/DorofeevaEMCY10] suggest.
The test suites are small since an ads can identify a state with a single word, instead of a set of words which is generally needed. The test suites are small since an ads can identify a state with a single word, instead of a set of words which is generally needed.
Even if the ads does not exist, using the partial result of Lee and Yannakakis' algorithm can reduce the size of test suites. Even if the ADS does not exist, using the partial result of Lee and Yannakakis' algorithm can reduce the size of test suites.
We will now see the construction of this hybrid method.
Instead of manipulating separating families directly, we use a \emph{splitting tree}. Instead of manipulating separating families directly, we use a \emph{splitting tree}.
This is a data structure which is used to construct separating families or adaptive distinguishing sequences. This is a data structure which is used to construct separating families or adaptive distinguishing sequences.
@ -470,7 +555,7 @@ A \defn{splitting tree (for $M$)} is a rooted tree where each node $u$ has
We require that if a node $u$ has children $C(u)$ then We require that if a node $u$ has children $C(u)$ then
\startitemize \startitemize
\item the sets of states of the children of $u$ partition $l(u)$, i.e., the set \item the sets of states of the children of $u$ partition $l(u)$, i.e., the set
$P(u) = \{l(v) \,|\, v \in C(u)\}$ is a \todo{non-trivial} partition of $l(u)$, and $P(u) = \{l(v) \,|\, v \in C(u)\}$ is a \emph{non-trivial} partition of $l(u)$, and
\item the sequence $\sigma(u)$ witnesses the partition $P(u)$, meaning that \item the sequence $\sigma(u)$ witnesses the partition $P(u)$, meaning that
$\lambda(s, \sigma(u)) = \lambda(t, \sigma(u))$ iff $p = q$ for all $s \in p, t \in q$ for all $p, q \in P(u)$. $\lambda(s, \sigma(u)) = \lambda(t, \sigma(u))$ iff $p = q$ for all $s \in p, t \in q$ for all $p, q \in P(u)$.
\stopitemize \stopitemize
@ -479,7 +564,7 @@ A splitting tree is called \defn{complete} if all inequivalent states belong to
Efficient construction of a splitting tree is described in more detail in \in{Chapter}[chap:minimal-separating-sequences]. Efficient construction of a splitting tree is described in more detail in \in{Chapter}[chap:minimal-separating-sequences].
Briefly, the splitting tree records the execution of a partition refinement algorithm (such as Moore's or Hopcroft's algorithm). Briefly, the splitting tree records the execution of a partition refinement algorithm (such as Moore's or Hopcroft's algorithm).
Each non-leaf node encode a \defn{split} together with a witness, which is a separating sequence for its children. Each non-leaf node encodes a \defn{split} together with a witness, which is a separating sequence for its children.
From such a tree we can construct a state identifier for a state by locating the leaf containing that state and collecting all the sequences you read when traversing to the root. From such a tree we can construct a state identifier for a state by locating the leaf containing that state and collecting all the sequences you read when traversing to the root.
For adaptive distinguishing sequences an additional requirement is put on the splitting tree: For adaptive distinguishing sequences an additional requirement is put on the splitting tree:
@ -487,33 +572,33 @@ for each non-leaf node $u$, the sequence $\sigma(u)$ defines an injective map $x
\cite[authoryears][DBLP:journals/tc/LeeY94] call such splits \defn{valid}. \cite[authoryears][DBLP:journals/tc/LeeY94] call such splits \defn{valid}.
\in{Figure}[fig:example-splitting-tree] shows both valid and invalid splits. \in{Figure}[fig:example-splitting-tree] shows both valid and invalid splits.
Validity precisely ensures that after performing a split, the states are still distinguishable. Validity precisely ensures that after performing a split, the states are still distinguishable.
Hence, such splits (or rather their sequences) can be concatenated.
\startplacefigure \startplacefigure
[title={A complete splitting tree with shortest witnesses for the specification of \in{Figure}[fig:running-example]. [title={A complete splitting tree with shortest witnesses for the specification of \in{Figure}[fig:running-example].
Only the splits $a$ and $aa$ are valid. Only the splits $a$, $aa$, and $ac$ are valid.},
\todo{Commands maken voor deze plaatjes.}},
list={Complete splitting tree with shortest witnesses for \in{Figure}[fig:running-example].}, list={Complete splitting tree with shortest witnesses for \in{Figure}[fig:running-example].},
reference=fig:example-splitting-tree] reference=fig:example-splitting-tree]
\hbox{ \hbox{
\starttikzpicture[node distance=1.5cm] \starttikzpicture[node distance=1.75cm]
\node (0) [text width=3cm, align=center, ] {$s_0, s_1, s_2, s_3, s_4$ $a$}; \splitnode{0}{s_0, s_1, s_2, s_3, s_4}{a}{}
\node (1) [text width=1cm, align=center, below left of=0 ] {$s_1$}; \splitnode{3}{s_0, s_2, s_3, s_4}{c}{below right of=0}
\node (2) [text width=2.5cm, align=center, below right of=0] {$s_0, s_2, s_3, s_4$ $b$}; \splitnode{5}{s_0, s_2, s_4}{aa}{below left of=3}
\node (3) [text width=2.0cm, align=center, below left of=2 ] {$s_0, s_2, s_3$ $c$}; \splitnode{8}{s_2, s_4}{ac}{below right of=5}
\node (4) [text width=1cm, align=center, below right of=2] {$s_4$}; \node (1) [below left of=0 ] {$s_1$};
\node (5) [text width=1.8cm, align=center, below left of=3 ] {$s_0, s_2$ $aa$}; \node (6) [below right of=3] {$s_3$};
\node (6) [text width=1cm, align=center, below right of=3] {$s_3$}; \node (7) [below left of=5 ] {$s_0$};
\node (7) [text width=1cm, align=center, below left of=5 ] {$s_0$}; \node (8l)[below left of=8 ] {$s_2$};
\node (8) [text width=1cm, align=center, below right of=5] {$s_2$}; \node (8r)[below right of=8] {$s_4$};
\path[->] \path[->]
(0) edge (1) (0) edge (1)
(0) edge (2) (0) edge (3)
(2) edge (3)
(2) edge (4)
(3) edge (5) (3) edge (5)
(3) edge (6) (3) edge (6)
(5) edge (7) (5) edge (7)
(5) edge (8); (5) edge (8)
(8) edge (8l)
(8) edge (8r);
\stoptikzpicture \stoptikzpicture
} }
\stopplacefigure \stopplacefigure
@ -528,43 +613,38 @@ Our method uses the exact same algorithm as the one by Lee and Yannakakis.
However, we also apply it in the case when the splitting tree with valid splits is not complete (and hence no adaptive distinguishing sequence exists). However, we also apply it in the case when the splitting tree with valid splits is not complete (and hence no adaptive distinguishing sequence exists).
Their algorithm still produces a family of sets, but is not necessarily a separating family. Their algorithm still produces a family of sets, but is not necessarily a separating family.
In order to recover separability, we refine that family of sets. In order to recover separability, we refine that family.
Let $\Fam{Z'}$ be the result of Lee and Yannakakis' algorithm (to distinguish from their notation, we add a prime) and let $\Fam{H}$ be a separating family extracted from an ordinary splitting tree. Let $\Fam{Z'}$ be the result of Lee and Yannakakis' algorithm (to distinguish from their notation, we add a prime) and let $\Fam{H}$ be a separating family extracted from an ordinary splitting tree.
The hybrid ADS family is defined as $\Fam{Z'} ; \Fam{H}$, and can be computed as sketched in \in{Algorithm}[alg:hybrid]. The hybrid ADS family is defined as $\Fam{Z'} ; \Fam{H}$, and can be computed as sketched in \in{Algorithm}[alg:hybrid] (the algorithm works on splitting trees instead of separating families).
\todo{Niet precies wat ik in de code doe (wel equivalent), omdat ik efficienter de boom doorloop. En $\Fam{Z,H}$ gegeven door splitting tree.}
By \in{Lemma}[lemma:refinement-props] we note the following: in the best case this family is an adaptive distinguishing sequence; in the worst case it is equal to $\Fam{H}$; and in general it is a combination of the two families. By \in{Lemma}[lemma:refinement-props] we note the following: in the best case this family is an adaptive distinguishing sequence; in the worst case it is equal to $\Fam{H}$; and in general it is a combination of the two families.
In all cases, the result is a separating family because $\Fam{H}$ is.
\startplacealgorithm \startplacealgorithm
[title={Obtaining the hybrid separating family $\Fam{Z'} ; \Fam{H}$}, [title={Obtaining the hybrid separating family $\Fam{Z'} ; \Fam{H}$},
reference=alg:hybrid] reference=alg:hybrid]
\startalgorithmic \startalgorithmic
\REQUIRE{A Mealy machine $M$} \REQUIRE{A Mealy machine $M$}
\ENSURE{A separating family $Z'$} \ENSURE{A separating family $Z$}
\startlinenumbering \startlinenumbering
\STATE $T_1 \gets$ splitting tree for Moore's minimisation algorithm \STATE $T_1 \gets$ splitting tree for Moore's minimisation algorithm
\STATE $\Fam{H} \gets$ separating family extracted from $T_1$ \STATE $T_2 \gets$ splitting tree with valid splits (see \citenp[DBLP:journals/tc/LeeY94])
\STATE $T_2 \gets$ splitting tree with valid splits (see \cite[DBLP:journals/tc/LeeY94]) \STATE $\Fam{Z'} \gets$ (incomplete) family constructed from $T_2$
\STATE $\Fam{Z'} \gets$ (incomplete) family as constructed from $T_2$
\FORALL{inequivalent states $s, t$ in the same leaf of $T_2$}{ \FORALL{inequivalent states $s, t$ in the same leaf of $T_2$}{
\STATE $u \gets lca(s, t)$ \STATE $u \gets lca(T_1, s, t)$
\STATE $Z'_s \gets Z_s \cup \{ \sigma(u) \}$ \STATE $Z_s \gets Z'_s \cup \{ \sigma(u) \}$
\STATE $Z'_t \gets Z_t \cup \{ \sigma(u) \}$ \STATE $Z_t \gets Z'_t \cup \{ \sigma(u) \}$
} }
\ENDFOR \ENDFOR
\RETURN{$Z'$} \RETURN{$Z$}
\stoplinenumbering \stoplinenumbering
\stopalgorithmic \stopalgorithmic
\stopplacealgorithm \stopplacealgorithm
With the hybrid family we can define the test suite as follows. With the hybrid family we can define the test suite as follows.
In words, the suite consists of tests of the form $p w s$, where $p$ brings the SUT to a certain state, $w$ is to detect $k$ extra states and $s$ is to identify the state.
Its $m$-completeness is proven in \in{Section}[sec:completeness]. Its $m$-completeness is proven in \in{Section}[sec:completeness].
\todo{https://gitlab.science.ru.nl/moerman/hybrid-ads}
\startdefinition \startdefinition
Let $P$ be a state cover, 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.
$\Fam{Z'}$ be a family of sets constructed with the Lee and Yannakakis algorithm and
let $\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 = P \cdot I^{\leq k+1} \odot (\Fam{Z'} ; \Fam{H}).
@ -572,27 +652,25 @@ T = P \cdot I^{\leq k+1} \odot (\Fam{Z'} ; \Fam{H}).
\stopdefinition \stopdefinition
\stopsubsection \startsubsection
\startsubsection[title={Example}] [title={Example},
reference=sec:hads-example]
\todo{Beter opschrijven, en uiteindelijke test suite geven.
En vergelijken met andere methode? Misschien later pas.}
In the figure we see the (unique) result of Lee and Yannakakis' algorithm. In the figure we see the (unique) result of Lee and Yannakakis' algorithm.
We note that the states $s_2, s_3, s_4$ are not split, so we need to refine the family for those states. We note that the states $s_2, s_3, s_4$ are not split, so we need to refine the family for those states.
\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 \cite[DBLP:journals/tc/LeeY94].}, (b): Its adaptive distinguishing tree in notation of \citet[DBLP:journals/tc/LeeY94].},
list={Splitting tree and adaptive distinguishing sequence.}, list={Splitting tree and adaptive distinguishing sequence.},
reference=fig:example-splitting-tree] reference=fig:example-splitting-tree]
\startcombination[2*1]{ \startcombination[2*1]{
\hbox{ \hbox{
\starttikzpicture[node distance=2.0cm] \starttikzpicture[node distance=2cm]
\node (0) [text width=2cm, align=center, ] {$s_0, s_1, s_2, s_3, s_4$ $a$}; \splitnode{0}{s_0, s_1, s_2, s_3, s_4}{a}{}
\node (1) [text width=1cm, align=center, below left of=0 ] {$s_1$}; \splitnode{2}{s_0, s_2, s_3, s_4}{aa}{below right of=0}
\node (2) [text width=2cm, align=center, below right of=0] {$s_0, s_2, s_3, s_4$ $aa$}; \node (1) [below left of=0 ] {$s_1$};
\node (3) [text width=1cm, align=center, below left of=2 ] {$s_0$}; \node (3) [below left of=2 ] {$s_0$};
\node (4) [text width=1cm, align=center, below right of=2] {$s_2, s_3, s_4$}; \node (4) [below right of=2] {$s_2, s_3, s_4$};
\path[->] \path[->]
(0) edge (1) (0) edge (1)
(0) edge (2) (0) edge (2)
@ -601,12 +679,12 @@ 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=2.0cm] \starttikzpicture[node distance=2cm]
\node (0) [text width=2cm, align=center, ] {$s_0, s_1, s_2, s_3, s_4$ $s_0, s_1, s_2, s_3, s_4$ $a$}; \adsnode{0}{s_0, s_1, s_2, s_3, s_4}{s_0, s_1, s_2, s_3, s_4}{a}{}
\node (1) [text width=1cm, align=center, below left of=0 ] {$s_1$ $s_2$}; \adsnode{1}{s_1}{s_2}{}{below left of=0}
\node (2) [text width=2cm, align=center, below right of=0] {$s_0, s_2, s_3, s_4$ $s_1, s_2, s_4, s_3$ $a$}; \adsnode{2}{s_0, s_2, s_3, s_4}{s_1, s_2, s_4, s_3}{aa}{below right of=0}
\node (3) [text width=1cm, align=center, below left of=2 ] {$s_0$ $s_2$}; \adsnode{3}{s_0}{s_2}{}{below left of=2}
\node (4) [text width=1cm, align=center, below right of=2] {$s_2, s_3, s_4$ $s_2, s_3, s_4$}; \adsnode{4}{s_2, s_3, s_4}{s_2, s_3, s_4}{}{below right of=2}
\path[->] \path[->]
(0) edge (1) (0) edge (1)
(0) edge (2) (0) edge (2)
@ -617,22 +695,45 @@ We note that the states $s_2, s_3, s_4$ are not split, so we need to refine the
\stopcombination \stopcombination
\stopplacefigure \stopplacefigure
\todo{Dit eerder noemen. En zeggen: we take the same $\Fam{H}$ as before.}
From the splitting tree in \in{Figure}[fig:example-splitting-tree], we obtain the following separating family $\Fam{H}$. From the splitting tree in \in{Figure}[fig:example-splitting-tree], we obtain the following separating family $\Fam{H}$.
From the figure 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:
\starttabulate[|l|l|l|] \starttabulate[|l|l|l|]
\NC $H_0 = \{aa,b,c\}$ \NC $Z'_0 = \{aa\}$ \NC $(Z';H)_0 = \{aa\}$ \NC\NR \NC $H_0 = \{aa,c\}$ \NC $Z'_0 = \{aa\}$ \NC $(Z';H)_0 = \{aa\}$ \NC\NR
\NC $H_1 = \{a\}$ \NC $Z'_1 = \{a\}$ \NC $(Z';H)_1 = \{a\}$ \NC\NR \NC $H_1 = \{a\}$ \NC $Z'_1 = \{a\}$ \NC $(Z';H)_1 = \{a\}$ \NC\NR
\NC $H_2 = \{aa,b,c\}$ \NC $Z'_2 = \{aa\}$ \NC $(Z';H)_2 = \{aa,b,c\}$ \NC\NR \NC $H_2 = \{aa,ac,c\}$ \NC $Z'_2 = \{aa\}$ \NC $(Z';H)_2 = \{aa,ac,c\}$ \NC\NR
\NC $H_3 = \{a,b,c\}$ \NC $Z'_3 = \{aa\}$ \NC $(Z';H)_3 = \{a,b,c\}$ \NC\NR \NC $H_3 = \{a,c\}$ \NC $Z'_3 = \{aa\}$ \NC $(Z';H)_3 = \{aa,c\}$ \NC\NR
\NC $H_4 = \{a,b\}$ \NC $Z'_4 = \{aa\}$ \NC $(Z';H)_4 = \{aa,b\}$ \NC\NR \NC $H_4 = \{aa,ac,c\}$ \NC $Z'_4 = \{aa\}$ \NC $(Z';H)_4 = \{aa,ac,c\}$ \NC\NR
\stoptabulate \stoptabulate
\todo{In startformula/startalign zetten} \todo{In startformula/startalign zetten}
With the separating family $\Fam{Z}'; \Fam{H}$ we obtain the following test suite of size 96:
\startformula
T_{\text{h-ADS}} = \{ \alignhere aaaaa, aaaac, aaac, aabaa, aacaa, abaa, acaa, \breakhere
baaaa, baaac, baac, babaa, bacaa, bacc, bbaa, bbac, \breakhere
bbc, bcaa, caa \} \breakhere
\stopformula
We note that this is indeed smaller than the HSI test suite.
In particular, we have a smaller state identifier for $s_0$: $\{ aa \}$ instead of $\{ aa, c \}$.
As a consequence, there are less combinations of prefixes and suffixes.
We also observe that one of the state identifiers grew in length: $\{ aa, c \}$ instead of $\{ a, c \}$ for state $s_3$.
\stopsubsection \stopsubsection
\startsubsection \startsubsection
[title={Implementation}]
All the algorithms concerning the hybrid ADS-method have been implemented and can be found at
\href{https://gitlab.science.ru.nl/moerman/hybrid-ads}.
We note that \in{Algorithm}[alg:hybrid] is implemented a bit more efficiently, as we can walk the splitting trees in a particular order.
For constructing the splitting trees in the first place, we use Moore's minimisation algorithm and the algorithms by \citet[DBLP:journals/tc/LeeY94].
\stopsubsection
\stopsection
\startsection
[title={Overview}, [title={Overview},
reference=sec:overview] reference=sec:overview]
@ -671,8 +772,7 @@ The following test suites are all $n+k$-complete:
\stoptabulate \stoptabulate
\stoptheorem \stoptheorem
\todo{Iets zeggen over de hybrid UIO method.} \todo{Iets zeggen over de hybrid UIO method?}
\todo{Geef groottes van suites voor het voorbeeld. Merk op dat ADS and UIOv niet van toepassing zijn (state 2 heeft geen UIO)}
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.
@ -684,14 +784,18 @@ Also we expect the bottom row to perform better as there is a single test for ea
Small experimental results confirm this intuition Small experimental results confirm this intuition
\cite[DBLP:journals/infsof/DorofeevaEMCY10]. \cite[DBLP:journals/infsof/DorofeevaEMCY10].
On the example in \in{Figure}[fig:running-example], we computed all applicable test suites in \in{Sections}[sec:all-example] and \in{}[sec:hads-example].
The UIO and ADS methods are not applicable.
For the W, Wp, HSI and hybrid ADS methods we obtained test suites of size 169, 75, 125 and 96 respectively.
\stopsubsection
\stopsection \stopsection
\startsection \startsection
[title={Proof of completeness}, [title={Proof of completeness},
reference=sec:completeness] reference=sec:completeness]
\todo{Stukje over bisimulaties?} \todo{Stukje over bisimulaties?}
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: We define the following notation:
@ -701,7 +805,7 @@ Let $W \subseteq I^{\ast}$ be a set of words.
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$. 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$.
\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 \Rightarrow x \sim_W y$. 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$.
The next lemma gives sufficient conditions for a test suite of the given anatomy to be The next lemma gives sufficient conditions for a test suite of the given anatomy 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 paper.
@ -748,9 +852,8 @@ 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 described in this paper, we reflect on the above proof first.
This proof is very similar to the completeness proof in \cite[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 in \cite[DBLP:journals/iandc/Angluin87] which proves termination in the L* learning algorithm. This correspondence was noted in \cite[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].)
\todo{Hoofdstuk over leren van nom. aut. heeft ook deze stelling.}
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.
Then in the second part we show the actual equivalence. Then in the second part we show the actual equivalence.
To the best of the authors knowledge, this is first $m$-completeness proof which explicitly uses the concept of a bisimulation. To the best of the authors knowledge, this is first $m$-completeness proof which explicitly uses the concept of a bisimulation.
@ -793,12 +896,10 @@ The HSI, ADS and hybrid ADS test suites are $n+k$-complete.
[title={Related Work and discussion}] [title={Related Work and discussion}]
\todo{Opnieuw lezen, want verouderd. Voeg toe: non-det, no-reset, transition tour, checking sequence. Future work: benchmarks (ref benchmark wiki).} \todo{Opnieuw lezen, want verouderd. Voeg toe: non-det, no-reset, transition tour, checking sequence. Future work: benchmarks (ref benchmark wiki).}
Comparison of test methods already appeared in the recent papers \cite[DBLP:journals/infsof/DorofeevaEMCY10] and \cite[DBLP:journals/infsof/EndoS13]. Comparison of test methods already appeared in the recent papers by \citet[DBLP:journals/infsof/DorofeevaEMCY10, DBLP:journals/infsof/EndoS13].
Their work is mainly evaluated on randomly generated Mealy machines. Their work is mainly evaluated on randomly generated Mealy machines.
We continue their work by evaluating on many specifications from industry.
In addition, we evaluate in the context of learning, which has been lacking so far.
Many of the methods describe here are benchmarked on small Mealy machines in \cite[DBLP:journals/infsof/DorofeevaEMCY10] and \cite[DBLP:journals/infsof/EndoS13]. Many of the methods described here are benchmarked on small Mealy machines in \cite[DBLP:journals/infsof/DorofeevaEMCY10] and \cite[DBLP:journals/infsof/EndoS13].
Additionally, they included the P, H an SPY methods. Additionally, they included the P, H an SPY methods.
Unfortunately, the P and H methods do not fit naturally in the overview presented in \in{Section}[sec:overview]. Unfortunately, the P and H methods do not fit naturally in the overview presented in \in{Section}[sec:overview].
The P method is not able to test for extra states, making it less usable. The P method is not able to test for extra states, making it less usable.
@ -814,11 +915,11 @@ This is a bit dual to our approach, as our \quotation{incomplete} adaptive disti
Our method becomes complete by refining the tests with pairwise separating sequences. Our method becomes complete by refining the tests with pairwise separating sequences.
Some work is put into minimizing the adaptive distinguishing sequences themselves. Some work is put into minimizing the adaptive distinguishing sequences themselves.
In \cite[DBLP:journals/fmsd/TurkerY14] the authors describe greedy algorithms which construct small adaptive distinguishing sequences. \citet[DBLP:journals/fmsd/TurkerY14] describe greedy algorithms which construct small adaptive distinguishing sequences.
\todo{We expect that similar \todo{We expect that similar
heuristics also exist for the other test methods and that it will improve the heuristics also exist for the other test methods and that it will improve the
performance.} performance.}
However, they show that finding the minimal adaptive distinguishing sequence is NP-complete, even approximation is NP-complete. However, they show that finding the minimal adaptive distinguishing sequence is NP-complete in general, even approximation is NP-complete.
We would like to incorporate their greedy algorithms in our implementation. We would like to incorporate their greedy algorithms in our implementation.
\todo{Noem minimal sep seqs. Dit is niet genoeg voor een minimal test suite.} \todo{Noem minimal sep seqs. Dit is niet genoeg voor een minimal test suite.}
@ -826,10 +927,10 @@ We would like to incorporate their greedy algorithms in our implementation.
\startsubsection \startsubsection
[title={When $k$ is not known}] [title={When $k$ is not known}]
In many of the applications described in \in{Section}[sec:applications] 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.
Still, for the applications in \in{Section}[sec:applications] it has worked well in finding flaws. Still, as we will see in \in{Chapter}[chap:applying-automata-learning], this can work really well.
We can randomly test cases as follows. We can randomly test cases as follows.
In the above definition for the hybrid ADS test suite we replace $I^{\leq k}$ by $I^{\ast}$ to obtain an infinite test suite. In the above definition for the hybrid ADS test suite we replace $I^{\leq k}$ by $I^{\ast}$ to obtain an infinite test suite.
@ -839,13 +940,11 @@ Then we sample tests as follows:
\item sample a word $w$ from $I^{\ast}$ with a geometric distribution, and \item sample a word $w$ from $I^{\ast}$ with a geometric distribution, and
\item sample uniformly from $(\Fam{Z'} ; \Fam{H})_s$ for the state $s = \delta(s_0, pw)$. \item sample uniformly from $(\Fam{Z'} ; \Fam{H})_s$ for the state $s = \delta(s_0, pw)$.
\stopitemize \stopitemize
This random testing method is also implemented in the \kw{hybrid ADS} tool.
\todo{Hoe te verwijzen?}
\stopsubsection \stopsubsection
\todo{Enkele resultaten bespreken, test-suite-groottes vergelijken}
\todo{Future work? Meer benchmarks? Andere automaat-modellen?}
\stopsection \stopsection
\referencesifcomponent \referencesifcomponent
\stopchapter \stopchapter

9
environment/tikz.tex
View file

@ -19,6 +19,15 @@
\draw ({(#1+#2)/2-0.5},{(3-#3)*0.75+0.65}) node[fill=white] (B#4) {{$B_{#4}$} {$\scriptscriptstyle #5$}}; \draw ({(#1+#2)/2-0.5},{(3-#3)*0.75+0.65}) node[fill=white] (B#4) {{$B_{#4}$} {$\scriptscriptstyle #5$}};
} }
\define[4]\splitnode{
\node (#1) [#4] {$#2$};
\node (#1s) [below=-2pt of #1] {$#3$};
}
\define[5]\adsnode{
\node (#1) [align=center,#5] {$I = #2$ \\ $C = #3$};
\node (#1s) [below=-2pt of #1] {$#4$};
}
% Used to draw extended cells in observation tables for the learning nominal automata paper % Used to draw extended cells in observation tables for the learning nominal automata paper
\define[1]\NomCell{ \define[1]\NomCell{
\startmathcases \startmathcases