Meer over test methods

content/test-methods.tex

@@ -6,13 +6,13 @@
    reference=chap:test-methods]
 
 In this chapter we will discuss some of the theory of test generation methods.
-From this 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]).
+From this 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]).
 A key aspect of such methods is the size of the obtained test suite.
 On one hand we want to cover as much as the specification as possible.
 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.
-They all share similar concepts, such as access sequences and 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.
 
 
@@ -20,10 +20,9 @@ In this chapter we will define these concepts, relate them with one another and
   [title={Mealy machines and sequences}]
 
 We will focus on Mealy machines, as those capture many protocol specifications and reactive systems.
-Note that we restrict ourselves to deterministic and complete machines.
 
 We fix finite alphabets $I$ and $O$ of inputs respectively outputs.
-We use the usual notation for operations on \emph{sequences} (also called words):
+We use the usual notation for operations on \emph{sequences} (also called \emph{words}):
 $uv$ for the concatenation of two sequences $u, v \in I^{\ast}$ and $|u|$ for the length of $u$.
 For a sequence $w = uv$ we say that $u$ and $v$ are a prefix and suffix respectively.
 
@@ -39,14 +38,18 @@ Both the transition function and output function are extended inductively to seq
 \NC \delta(s, \epsilon) \NC = s \NC\quad \lambda(s, \epsilon) \NC = \epsilon \NR
 \NC \delta(s, aw) \NC = \delta(\delta(s, a), w) \NC\qquad \lambda(s, aw) \NC = \lambda(s, a)\lambda(\delta(s, a), w) \NR
 \stopmathmatrix\stopformula
-By abuse of notation we will often write $s \in M$ instead of $s \in S$.
-For a second Mealy machine $M'$ its members are denoted $S', s'_0, \delta'$ and $\lambda'$ by convention.
 
 The \emph{behaviour} of a state $s$ is given by the output function $\lambda(s, -) \colon I^{\ast} \to O^{\ast}$.
 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
 
-\todo{Conventie: $x$ hoort bij een unieke $M$.}
+\startremark
+We will use the following conventions and notation.
+We often write $s \in M$ instead of $s \in S$ and for a second Mealy machine $M'$ its members are denoted $S', s'_0, \delta'$ and $\lambda'$.
+Moreover, if we have a state $s \in M$, we silently assume that $s$ is not a member of any other Mealy machine $M'$.
+(In other words, the behaviour of $s$ is determined by the state itself.)
+This eases the notation since we can write $s \sim t$ without needing to introduce a context.
+\stopremark
 
 An example Mealy machine is given in \in{Figure}[fig:running-example].
 We note that a Mealy machine is deterministic and complete by definition.
@@ -93,7 +96,7 @@ If the output is different than the specified output, then we know the implement
 The goals is to test as little as possible, while covering as much as possible.
 
 We assume the following
-\startitemize
+\startitemize[after]
 \item
 The system can be modelled as Mealy machine.
 In particular, this means it is \emph{deterministic} and \emph{complete}.
@@ -101,16 +104,18 @@ In particular, this means it is \emph{deterministic} and \emph{complete}.
 We are able to reset the system, i.e., bring it back to the initial state.
 \stopitemize
 
+A test suite is nothing more than a set of sequences.
+We do not have to encode outputs in the test suite, as those follow from the deterministic specification.
+
 \startdefinition[reference=test-suite]
 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 test $s \in T$.
-We denote the set of maximal tests of $T$ with $max(T)$.
+We denote the set of maximal tests of $T$ by $\max(T)$.
-\todo{Conventie: Alles is prefix closed. Behalve in de voorbeelden en implementatie.}
-
 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.
+In the examples of this chapter we will show $\max(T)$ instead of $T$.
+
 We define the size of a test suite as usual \citep[DBLP:journals/infsof/DorofeevaEMCY10, DBLP:conf/hase/Petrenko0GHO14].
 The size of a test suite is measured as the sum of the lengths of all its maximal tests plus one reset per test.
 
@@ -209,25 +214,40 @@ In order to separate $s_2$ from the other state, we have to pick multiple sequen
 For instance, the set $\{aa, ac, c\}$ will separate $s_2$ from all other states.
 \stopexample
 
-\startdefinition
+
-As the example shows, we need sets of sequences and sometimes even sets of sets of sqeuences -- called \emph{families}.
+\stopsubsection
+\startsubsection
+  [title={Sets of separating sequences}]
+
+As the example shows, we need sets of sequences and sometimes even sets of sets of sequences -- 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$.}
+
+\startdefinition
 Given a Mealy machine $M$, we define the following kinds of sets of sequences.
-\todo{Alles eindig?}
+We require that all sets are \emph{prefix-closed}, however, we only give the maximal sequences in examples.
+\footnote{Taking these sets to be prefix-closed makes many proofs easier.}
 \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 in $M$.
-\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 \in M$ is a set $W_s$ which contains a separating sequence for every other state $t \in M$.
 \item A set of state identifiers $\{ W_s \}_{s}$ is \defn{harmonised} if a separating sequence $w$ for states $s$ and $t$ exists in both $W_s$ and $W_t$.
-This is sometimes called a \defn{separating family}.
+This is also called a \defn{separating family}.
-\todo{Equivalently: $x \sim_\Fam{X} y$ implies $x \sim y$}
+\item 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).
-\todo{Preciezer zijn over prefixes...}
-\item Following the definitions of \citet[DBLP:journals/tc/LeeY94], a separating family where each set is a singleton is an \defn{adaptive distinguishing sequence} (ADS).
-An ads is of special interest since they can identify a state using a single word.
 \stopitemize
 \stopdefinition
 
-These notions are again related.
+The property of being harmonised might seem a bit strange.
-We obtain a characterisation set by taking the union of state identifiers for each state.
+This property ensure that the same tests are used for different states.
+This extra consistency within a test suite is necessary for some test methods.
+A counterexample is given in \in{Example}[ex:uio-counterexample].
+
+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.
+To see this, 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.
+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).
+\todo{plaatje?}
+
+We may 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.
 However, an adaptive distinguishing sequence may not exist, even if every state has an UIO.
 
@@ -235,16 +255,18 @@ However, an adaptive distinguishing sequence may not exist, even if every state
 As mentioned before, state $s_2$ from \in{Figure}[fig:running-example] has a state identifier $\{aa, ac, b\}$.
 In fact, this set is a characterisation set for the whole machine.
 Since the other states have UIOs, we can pick singleton sets as state identifiers.
-For example, state $s_0$ has the UIO $aa$, so a state identifier for $s_0$ is $\{ aa \}$.
+For example, state $s_0$ has the UIO $aa$, so a state identifier for $s_0$ is $W_0 = \{ aa \}$.
+Similarly, we can take $W_1 = \{ a \}$ and $W_3 = \{ c \}$.
+But note that such a family will \emph{not} be harmonised since the sets $\{ a \}$ and $\{ c \}$ have no common separating sequence.
 There is no ADS for this machine.
 \stopexample
 
 Besides sequences which separate states, we also need sequences which brings a machine to specified states.
 
 \startdefinition
-An \emph{access sequence for state $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(q_0, w) = s$.
 A set $P$ consisting of an access sequence for each state is called a \emph{state cover}.
-If $P$ is a state cover, $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
 
 
@@ -253,29 +275,21 @@ If $P$ is a state cover, $P \cdot I$ is called a \emph{transition cover}.
   [title={Constructions on sets of sequences}]
 
 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:
+We fix a specification $M$.
-\todo{Nog eens herhalen dat het prefix closed is?}
+For sets of words $X$ and $Y$, we define
-
 \startitemize[after]
 \item their concatenation $X \cdot Y = \{ xy \mid x \in X, y \in Y \}$,
-\item iterated concatenation $X^0 = \{ \epsilon \}$ and $X^{n+1} = X \cdot X^{n}$,
+\item iterated concatenation $X^0 = \{ \epsilon \}$ and $X^{n+1} = X \cdot X^{n}$, and
-\item bounded concatenation $X^{\leq n} = \bigcup_{i \leq n} X^i$, and
+\item bounded concatenation $X^{\leq n} = \bigcup_{i \leq n} X^i$.
-\item prefix closure $\pref(X) = \{ y \mid y \text{ is a prefix of } x, x \in X \}$.
 \stopitemize
 
-On families we define:
+On families we define
 \startitemize[after]
 \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:
 $(\Fam{X} \cup \Fam{Y})_s = X_s \cup Y_s$, and
 \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$.
-\todo{Hangt af van $M$, maar is nog niet gefixed}
-\stopitemize
-
-Given a specification $M$ we define two operations.
-We omit $M$ from the notation as the specification is always clear from the context.
-\startitemize[after]
 \item concatenation:
 $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
@@ -285,6 +299,8 @@ $X \odot \Fam{Y} = \{ xy \mid x \in X, y \in Y_{\delta(s_0, x)} \}$ and
 \stopitemize
 
 The latter construction is new and will be used to define a hybrid test generation method in \in{Section}[sec:hybrid].
+It refines a family $\Fam{X}$, which need not be separating, by including sequences from a second family $\Fam{Y}$.
+It only adds those sequences to states if $\Fam{X}$ does not distinguish those states.
 
 \startlemma[reference=lemma:refinement-props]
 For all families $\Fam{X}$ and $\Fam{Y}$:
@@ -305,14 +321,14 @@ For all families $\Fam{X}$ and $\Fam{Y}$:
   [title={Test generation methods},
    reference=sec:methods]
 
-In this section, we briefly review the classical conformance testing methods:
+In this section, we review the classical conformance testing methods:
 the W, Wp, UIO, UIOv, HSI, ADS methods.
-Our hybrid ADS method described is very similar to some of these methods, so we will relate them by describing them uniformly.
+Our hybrid ADS method uses a similar construction.
 
 There are many more test generation methods.
 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 that reason, completeness of the correct methods is shown in the next section.
+For that reason, completeness of the correct methods is shown in \in{Theorem}[thm:completeness].
 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$.
 
@@ -379,7 +395,6 @@ Let $\Fam{H}$ be a separating family, the \defn{HSI test suite} is defined as
 Our newly described test method is an instance of the HSI-method.
 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.
-In present paper that is generalised, allowing for our extension to be an instance.
 
 
 \stopsubsection
@@ -418,8 +433,13 @@ P \cdot I^{\leq k} \cdot \bigcup \Fam{U} \,\cup\, Q \cdot I^{\leq k} \odot \Fam{
 \stopdefinition
 
 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 \emph{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 following is a counterexample to such conjecture.
+(This counterexample is due to \citenp[DBLP:conf/sigcomm/ChanVO89].)
+
+\startexample
+  [reference=ex:uio-counterexample]
+The example in \in{Figure}[fig:uio-counterexample] shows that UIO-method does not define a 3-complete test suite.
 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.
 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$.
@@ -456,6 +476,7 @@ With the same UIOs as above, the resulting UIOv test suite for the specification
 \stoptikzpicture}} {Implementation}
 \stopcombination
 \stopplacefigure
+\stopexample
 
 
 \stopsubsection
@@ -523,6 +544,8 @@ 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.
 
+\todo{Draaien op faulty implementation}
+
 
 \stopsubsection
 \stopsection
@@ -571,7 +594,7 @@ 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}.
 \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.
-Hence, such splits (or rather their sequences) can be concatenated.
+Hence, sequences of such splits can be concatenated.
 
 \startplacefigure
   [title={A complete splitting tree with shortest witnesses for the specification of \in{Figure}[fig:running-example].
@@ -727,17 +750,18 @@ All the algorithms concerning the hybrid ADS-method have been implemented and ca
 \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].
+We keep all relevant sets prefix-closed by maintaining a \emph{trie data structure}.
+A trie data structure also allows us to immediately obtain the set of maximal tests only.
 
 
 \stopsubsection
 \startsubsection
-  [title={When $k$ is not known}]
+  [title={Randomisation}]
 
 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.
 Unfortunately, we lose the theoretical guarantees of completeness with random generation.
 Still, as we will see in \in{Chapter}[chap:applying-automata-learning], this can work really well.
-
 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.
 Then we sample tests as follows:
@@ -913,6 +937,8 @@ The HSI, ADS and hybrid ADS test suites are $n+k$-complete.
 \startsection
   [title={Related Work and Discussion}]
 
+\todo{Veel gerelateerd werk kan naar de grote intro.}
+
 In this chapter we have mostly considered classical test methods which are all based on prefixes and state identifiers.
 There are more recent methods which almost fit in the same framework.
 We mention the P \citep[SimaoP10], H \citep[DorofeevaEY05], and SPY \citep[SimaoPY09] methods.

environment/headers.tex

@@ -26,7 +26,7 @@
 \defineenumeration[theorem][text=Theorem]
 \defineenumeration[corollary][text=Corollary]
 \setupenumeration[definition,remark,example,lemma,proposition,theorem,corollary]
-  [alternative=serried, width=fit, right=., counter=lemmata]
+  [alternative=serried, width=fit, right=., counter=lemmata, indenting=yes]
 
 % Don't reset sections in new part
 \definestructureresetset[default][1,0,1][1] % reset part, not chapter, section