joshua/phd-thesis
Archived
1
Fork 0
Code Activity

Alle todos afgewerkt

Browse source
This commit is contained in:
Joshua Moerman 2019-01-07 09:13:06 +01:00
parent 65638971d3
commit fbb9a1b941
4 changed files with 43 additions and 32 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
content.tex
View file

@ -11,7 +11,7 @@
\midaligned{\framed[width=12cm,align=center,offset=2cm,frame=off]{Nominal Techniques \& Black Box Testing for Automata Learning}} \midaligned{\framed[width=12cm,align=center,offset=2cm,frame=off]{Nominal Techniques \& Black Box Testing for Automata Learning}}
\switchtobodyfont[12pt] \switchtobodyfont[12pt]
\midaligned{Joshua Moerman} \midaligned{Joshua Moerman}
\midaligned{draft New Year 2019} \midaligned{7 January 2019}
\stop \stop
\page[yes] \page[yes]

6
content/introduction.tex
View file

@ -607,6 +607,12 @@ The methods discussed in this thesis are all black box methods, this could be co
Often, we do have (parts of the) source code and we do know relationships between different inputs. Often, we do have (parts of the) source code and we do know relationships between different inputs.
The question is how this additional information can be integrated in a principled manner in the learning and testing of systems. The question is how this additional information can be integrated in a principled manner in the learning and testing of systems.
Black box testing still has theoretical challenges.
Current generalisations to non-deterministic systems or language inclusion (such as black box testing for IOCO) often need exponentially big test suites.
Whether this is necessary is unknown (to me), we only have upper bounds but no lower bounds.
An interesting approach would be to see if there exists a notion of reduction between test suites.
This is analogous to the reductions used complexity theory to prove problems hard, or reductions used in PAC theory to prove learning problems to be inherently unpredictable.
Another path taken in this thesis is the research on nominal automata. Another path taken in this thesis is the research on nominal automata.
This was motivated by the problem of learning automata over infinite alphabets. This was motivated by the problem of learning automata over infinite alphabets.
So far, the results on nominal automata are mostly theoretical in nature. So far, the results on nominal automata are mostly theoretical in nature.

65
content/test-methods.tex
View file

@ -191,24 +191,25 @@ This is crucial for black box testing, as we do not know the implementation, so
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.
We fix a Mealy machine $M$ for the remainder of this chapter. We fix a Mealy machine $M$ for the remainder of this chapter.
For convenience, we assume $M$ to be minimal, so that distinct states are, in fact, inequivalent.
(Or put differently: $s \sim t$ implies $s = t$.)
All definitions can be generalised to non-minimal $M$, by replacing the word \quote{distinct} (or \quote{other}) with \quote{inequivalent}.
\startdefinition \startdefinition
We define the following kinds of sequences. We define the following kinds of sequences.
\startitemize \startitemize
\item Given two states $s, t$ in $M$ we say that $w$ is a \defn{separating sequence} if $\lambda(s, w) \neq \lambda(t, w)$. \item Given two states $s, t$ in $M$ we say that $w$ is a \defn{separating sequence} if $\lambda(s, w) \neq \lambda(t, w)$.
\item For a single state $s$ in $M$, a sequence $w$ is a \defn{unique input output sequence (UIO)} if for every other state $t$ in $M$ we have $\lambda(s, w) \neq \lambda(t, w)$. \item For a single state $s$ in $M$, a sequence $w$ is a \defn{unique input output sequence (UIO)} if for every inequivalent state $t$ in $M$ we have $\lambda(s, w) \neq \lambda(t, w)$.
\item Finally, a \defn{(preset) distinguishing sequence (DS)} is a single sequence $w$ which separates all states of $M$, i.e., for every distinct pair $s, t$ in $M$ we have $\lambda(s, w) \neq \lambda(t, w)$. \item Finally, a \defn{(preset) distinguishing sequence (DS)} is a single sequence $w$ which separates all states of $M$, i.e., for every pair of inequivalent states $s, t$ in $M$ we have $\lambda(s, w) \neq \lambda(t, w)$.
\stopitemize \stopitemize
\stopdefinition \stopdefinition
The above list is ordered from weaker to stronger notions, i.e., every distinguishing sequence is an UIO sequence for every state. The above list is ordered from weaker to stronger notions, i.e., every distinguishing sequence is an UIO sequence for every state.
Similarly, an UIO for a state $s$ is a separating sequence for $s$ and any other $t$. Similarly, an UIO for a state $s$ is a separating sequence for $s$ and any inequivalent $t$.
Separating sequences always exist for inequivalent states and finding them efficiently is the topic of \in{Chapter}[chap:separating-sequences]. Separating sequences always exist for inequivalent states and finding them efficiently is the topic of \in{Chapter}[chap:separating-sequences].
On the other hand, UIOs and DSs do not always exist for a machine. On the other hand, UIOs and DSs do not always exist for a machine.
A machine $M$ is \emph{minimal} if every distinct pair of states is inequivalent (i.e.,\break $s \sim t \implies s = t$).
We will not require $M$ te be minimal, although this is often done in literature.
Minimality is sometimes convenient, as one can write \quote{every other state $t$} instead of \quote{every inequivalent state $t$}.
\startexample \startexample
For the machine in \in{Figure}[fig:running-example], we note that state $s_0$ and $s_2$ are separated by the sequence $aa$ (but not by any shorter sequence). For the machine in \in{Figure}[fig:running-example], we note that state $s_0$ and $s_2$ are separated by the sequence $aa$ (but not by any shorter sequence).
In fact, the sequence $aa$ is an UIO for state $s_0$ since it is the only state outputting $10$ on that input. In fact, the sequence $aa$ is an UIO for state $s_0$ since it is the only state outputting $10$ on that input.
@ -236,9 +237,9 @@ We define the following kinds of sets of sequences.
We require that all sets are \emph{prefix-closed}, however, we only show 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 inequivalent states in $M$.
\item A \defn{state identifier} for a state $s \in M$ is a set $W_s$ such that for every $t \in M$ a separating sequence for $s$ and $t$ exists in $W_s$. \item A \defn{state identifier} for a state $s \in M$ is a set $W_s$ such that for every inequivalent $t \in M$ a separating sequence for $s$ and $t$ exists in $W_s$.
\item A set of state identifiers $\{ W_s \}_{s}$ is \defn{harmonised} if $W_s \cap W_t$ contains a separating sequence for states $s$ and $t$. \item A set of state identifiers $\{ W_s \}_{s}$ is \defn{harmonised} if $W_s \cap W_t$ contains a separating sequence for inequivalent states $s$ and $t$.
This is also called a \defn{separating family}. This is also called a \defn{separating family}.
\stopitemize \stopitemize
\stopdefinition \stopdefinition
@ -372,16 +373,19 @@ $W$ is a characterisation set if and only if for all $s, t$ in $M$, $s \sim_W t$
$\Fam{W}$ is a separating family if and only if for all $s, t$ in $M$, $s \sim_{\Fam{W}} t$ implies $s \sim t$. $\Fam{W}$ is a separating family if and only if for all $s, t$ in $M$, $s \sim_{\Fam{W}} t$ implies $s \sim t$.
\stopitemize \stopitemize
\stoplemma \stoplemma
\startproof \startproofnoqed
\todo{Verhelderen (zie ook Sectie 5)}
\startitemize \startitemize
\item \item
$W$ is a characterisation set by definition means $s \not\sim t \implies s \not\sim_W t$ as $W$ contains a separating sequence (if it exists at all). $W$ is a characterisation set by definition means $s \not\sim t \implies s \not\sim_W t$ as $W$ contains a separating sequence (if it exists at all).
This is equivalent to $s \sim_W t \implies s \sim t$. This is equivalent to $s \sim_W t \implies s \sim t$.
\item \item
The same argument holds for a separating family by considering $W_s \cap W_t$. Let $\Fam{W}$ be a separating family and $s \not\sim t$.
Then there is a sequence $w \in W_s \cap W_t$ such that $\lambda(s, w) \neq \lambda(t, w)$, i.e., $s \not\sim_{\Fam{W}} t$.
We have shown $s \not\sim t \implies s \not\sim_{\Fam{W}} t$, which is equivalent to $s \sim_{\Fam{W}} t \implies s \sim t$.
The converse is proven similarly.
\QED
\stopitemize \stopitemize
\stopproof \stopproofnoqed
\stopsubsection \stopsubsection
@ -491,8 +495,8 @@ After the work of \citet[Moore56], it was unclear whether a test suite of polyno
He presented a finite test suite which was complete, however it was exponential in size. He presented a finite test suite which was complete, however it was exponential in size.
Both \citet[Chow78, Vasilevskii73] independently prove that test suites of polynomial size exist. Both \citet[Chow78, Vasilevskii73] independently prove that test suites of polynomial size exist.
\footnote{More precisely: the size of $T_{\text{W}}$ is polynomial in the size of the specification for each fixed $k$.} \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. The W-method is a very structured test suite construction.
It is called the W method as the characterisation set is often called $W$. It is called the W-method as the characterisation set is often called $W$.
\startdefinition \startdefinition
[reference=w-method] [reference=w-method]
@ -514,7 +518,7 @@ Together, these two phases put enough constraints on the implementation to know
[title={The Wp-method \cite[FujiwaraBKAG91]}, [title={The Wp-method \cite[FujiwaraBKAG91]},
reference=sec:wp] reference=sec:wp]
\citet[FujiwaraBKAG91] realised that one needs fewer tests in the second phase of the W method. \citet[FujiwaraBKAG91] realised that one needs fewer tests in the second phase of the W-method.
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. 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. This justifies the use of state identifiers for each state.
@ -553,7 +557,7 @@ T_{\text{HSI}} = (P \cup Q) \cdot I^{\leq k} \odot \Fam{H}.
Our hybrid ADS method is an instance of the HSI-method as we define it here. Our hybrid ADS method is an instance of the HSI-method as we define it here.
However, \citet[LuoPB95, PetrenkoYLD93] describe the HSI-method together with a specific way of generating the separating families. However, \citet[LuoPB95, PetrenkoYLD93] 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.
The hybrid ADS method does not refine the HSI method defined in the more restricted sense. The hybrid ADS method does not refine the HSI-method defined in the more restricted sense.
\stopsubsection \stopsubsection
@ -607,7 +611,7 @@ With the same UIOs as above, the resulting UIOv test suite for the specification
(Recall that we also count resets when measuring the size.) (Recall that we also count resets when measuring the size.)
\startplacefigure \startplacefigure
[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[nx=2, distance=1cm] \startcombination[nx=2, distance=1cm]
{\hbox{\starttikzpicture[node distance=2.5cm, bend angle=18] {\hbox{\starttikzpicture[node distance=2.5cm, bend angle=18]
@ -647,7 +651,7 @@ With the same UIOs as above, the resulting UIOv test suite for the specification
Let us compute all the previous test suites on the specification in \in{Figure}[fig:running-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 will be testing without extra states, i.e., we construct 5-complete test suites.
We start by defining the state and transition cover. 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. For this, we take all shortest sequences from the initial state to the other states.
This state cover is depicted in \in{Figure}[fig:running-example-prefixes]. This state cover is depicted in \in{Figure}[fig:running-example-prefixes].
The transition cover is simply constructed by extending each access sequence with another symbol. The transition cover is simply constructed by extending each access sequence with another symbol.
@ -715,7 +719,7 @@ All in all we get a test suite of size 75:
\NC \NC acaa, baaac, baac, babaa, bacc, bbac, bcaa, caa \quad \} \NR \NC \NC acaa, baaac, baac, babaa, bacc, bbac, bcaa, caa \quad \} \NR
\stopmathmatrix\stopformula \stopmathmatrix\stopformula
For the HSI method we need a separating family $\Fam{H}$. For the HSI-method we need a separating family $\Fam{H}$.
We pick the following sets: We pick the following sets:
\startformulas \startformulas
\startformula H_0 = \{ aa, c \} \stopformula \startformula H_0 = \{ aa, c \} \stopformula
@ -734,11 +738,11 @@ When combining this with the corresponding prefixes, we obtain the HSI test suit
\NC \NC abaa, abc, acaa, acc, baaaa, baaac, baac, babaa, \NR \NC \NC abaa, abc, acaa, acc, baaaa, baaac, baac, babaa, \NR
\NC \NC babc, baca, bacc, bbaa, bbac, bbc, bcaa, bcc, caa, cc \quad \} \NR \NC \NC babc, baca, bacc, bbaa, bbac, bbc, bcaa, bcc, caa, cc \quad \} \NR
\stopmathmatrix\stopformula \stopmathmatrix\stopformula
On this particular example the Wp method outperforms the HSI method. 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. 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). 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.
\startplacefigure \startplacefigure
[title={A faulty implementation for the specification in \in{Figure}[fig:running-example].}, [title={A faulty implementation for the specification in \in{Figure}[fig:running-example].},
@ -1037,6 +1041,7 @@ We classify them in two directions,
\starttheorem \starttheorem
[reference=thm:completeness] [reference=thm:completeness]
Assume $M$ to be minimal and of size $n$.
The following test suites are all $n+k$-complete: The following test suites are all $n+k$-complete:
\placetable[force,none]{}{ \placetable[force,none]{}{
@ -1063,8 +1068,12 @@ The following test suites are all $n+k$-complete:
\NR \HL %---------------------------------------- \NR \HL %----------------------------------------
\stoptabulate} \stoptabulate}
\stoptheorem \stoptheorem
\startproof
See \in{Corollary}[cor:w-wp-uiov-coplete] and \in{}[cor:hsi-ads-coplete].
\stopproof
Each of the methods in the right column can be written simpler as $P \cdot I^{\leq k+1} \odot \Fam{H}$, since $Q = P \cdot I$. Each of the methods in the right column can be written simpler as $P \cdot I^{\leq k+1} \odot \Fam{H}$, since $Q = P \cdot I$.
This makes them very easy to implement.
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.
@ -1179,8 +1188,6 @@ 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.
Using a bisimulation allows us to slightly generalise and use bisimulation up-to equivalence, dropping the the often-assumed requirement that $M$ is minimal. Using a bisimulation allows us to slightly generalise and use bisimulation up-to equivalence, dropping the the often-assumed requirement that $M$ is minimal.
\todo{Refer naar lemma uit eerste sectie}.
\startlemma \startlemma
Let $\Fam{W'}$ be a family of state identifiers for $M$. Let $\Fam{W'}$ be a family of state identifiers for $M$.
Define the family $\Fam{W}$ by $W_s = \bigcup \Fam{W'}$. Define the family $\Fam{W}$ by $W_s = \bigcup \Fam{W'}$.
@ -1194,7 +1201,7 @@ Then we note that $W'_y \subseteq \bigcup{W'}$ and so we get $x \sim_{W'_y} z \s
By transitivity we get $x \sim_{W'_y} y$ and so by definition of state identifier we get $x \sim y$. By transitivity we get $x \sim_{W'_y} y$ and so by definition of state identifier we get $x \sim y$.
\stopproof \stopproof
\startcorollary \startcorollary[reference=cor:w-wp-uiov-coplete]
The W, Wp, and UIOv test suites are $n+k$-complete. The W, Wp, and UIOv test suites are $n+k$-complete.
\stopcorollary \stopcorollary
@ -1208,7 +1215,7 @@ For the second condition, let $x \sim_{H_x} z \sim_{H_y} y$.
Then we get $x \sim_{H_x \cap H_y} z \sim_{H_x \cap H_y} y$ and so by transitivity $x \sim_{H_x \cap H_y} y$, hence again $x \sim y$. Then we get $x \sim_{H_x \cap H_y} z \sim_{H_x \cap H_y} y$ and so by transitivity $x \sim_{H_x \cap H_y} y$, hence again $x \sim y$.
\stopproof \stopproof
\startcorollary \startcorollary[reference=cor:hsi-ads-coplete]
The HSI, ADS and hybrid ADS test suites are $n+k$-complete. The HSI, ADS and hybrid ADS test suites are $n+k$-complete.
\stopcorollary \stopcorollary
@ -1218,14 +1225,12 @@ The HSI, ADS and hybrid ADS test suites are $n+k$-complete.
[title={Related Work and Discussion}, [title={Related Work and Discussion},
reference=sec:discussion] reference=sec: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. 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. 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. We mention the P \citep[SimaoP10], H \citep[DorofeevaEY05], and SPY \citep[SimaoPY09] methods.
The P method construct a test suite by carefully considering sufficient conditions for a $p$-complete test suite (here $p \leq n$, where $n$ is the number of states). The P method construct a test suite by carefully considering sufficient conditions for a $p$-complete test suite (here $p \leq n$, where $n$ is the number of states).
It does not generalise to extra states, but it seems to construct very small test suites. It does not generalise to extra states, but it seems to construct very small test suites.
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 chapter. We believe that this technique is independent of the HSI-method and can in fact be applied to all methods presented in this chapter.
@ -1242,7 +1247,7 @@ Some work is put into minimising the adaptive distinguishing sequences themselve
Moreover, they show that finding the minimal adaptive distinguishing sequence is NP-complete in general, even approximation is NP-complete. Moreover, they show that finding the minimal adaptive distinguishing sequence is NP-complete in general, even approximation is NP-complete.
We expect that similar heuristics also exist for the other test methods and that they will improve the performance. We expect that similar heuristics also exist for the other test methods and that they will improve the performance.
Note that minimal separating sequences do not guarantee a minimal test suite. Note that minimal separating sequences do not guarantee a minimal test suite.
In fact, we see that the hybrid ADS method outperforms the HSI method on the example in \in{Figure}[fig:running-example] since it prefers longer, but fewer, sequences. In fact, we see that the hybrid ADS method outperforms the HSI-method on the example in \in{Figure}[fig:running-example] since it prefers longer, but fewer, sequences.
Some of the assumptions made at the start of this chapter have also been challenged. Some of the assumptions made at the start of this chapter have also been challenged.
For non-deterministic Mealy machine, we mention the work of \citet[PetrenkoY14]. For non-deterministic Mealy machine, we mention the work of \citet[PetrenkoY14].

2
environment.tex
View file

@ -6,7 +6,7 @@
\setupexternalfigures[directory={images,../images}] \setupexternalfigures[directory={images,../images}]
% \definemode[afloop][yes] % \definemode[afloop][yes]
\definemode[draft][yes] % \definemode[draft][yes]
\environment bib \environment bib
\environment font \environment font