From aeb60d84cfd584a0109b37e00af2275614c04262 Mon Sep 17 00:00:00 2001 From: Joshua Moerman Date: Wed, 29 Apr 2015 15:42:19 +0200 Subject: [PATCH] Updates the docs a bit (to reflect the SJVM15 paper) --- docs/test_selection.tex | 93 ++++++++++++++++++----------------------- 1 file changed, 41 insertions(+), 52 deletions(-) diff --git a/docs/test_selection.tex b/docs/test_selection.tex index f97ed63..dc03275 100644 --- a/docs/test_selection.tex +++ b/docs/test_selection.tex @@ -1,72 +1,61 @@ -# Test selection strategies +\subsubsection{Augmented DS-method} +\label{sec:randomPrefix} - - - -## Augmented DS-method - -In order to perform less tests Chow and Vasilevski [...] pioneered the so called -W-method. In their framework a test query consists of a prefix $p$ bringing the -SUL to a specific state, a (random) middle part $m$ and a suffix $s$ asserting -that the SUL is in the appropriate state. This results in a test suite of the -form $P I^{\leq k} W$, where $P$ is a set of (shortest) access sequences, -$I^{\leq k}$ the set of all sequences of length at most $k$ and $W$ is the -characterization set. Classically, this characterization set is constructed by -taking the set of all (pairwise) separating sequences. For $k=1$ this test suite -is complete in the sense that if the SUL passes all tests, then either the SUL -is equivalent to the specification or the SUL has strictly more states than the -specification. By increasing $k$ we can check additional states. +In order to reduce the number of tests, Chow~\cite{Ch78} and +Vasilevskii~\cite{vasilevskii1973failure} pioneered the so called W-method. In +their framework a test query consists of a prefix $p$ bringing the SUL to a +specific state, a (random) middle part $m$ and a suffix $s$ assuring that the +SUL is in the appropriate state. This results in a test suite of the form $P +I^{\leq k} W$, where $P$ is a set of (shortest) access sequences, $I^{\leq k}$ +the set of all sequences of length at most $k$, and $W$ is a characterization +set. Classically, this characterization set is constructed by taking the set of +all (pairwise) separating sequences. For $k=1$ this test suite is complete in +the sense that if the SUL passes all tests, then either the SUL is equivalent to +the specification or the SUL has strictly more states than the specification. By +increasing $k$ we can check additional states. +We tried using the W-method as implemented by LearnLib to find counterexamples. The generated test suite, however, was still too big in our learning context. -Fujiwara observed that it is possible to let the set $W$ depend on the state the -SUL is supposed to be [...]. This allows us to only take a subset of $W$ which +Fujiwara et al \cite{FBKAG91} observed that it is possible to let the set $W$ depend on the state the +SUL is supposed to be. This allows us to only take a subset of $W$ which is relevant for a specific state. This slightly reduces the test suite which is as powerful as the full test suite. This methods is known as the Wp-method. More importantly, this observation allows for generalizations where we can carefully pick the suffixes. -In the presence of an (adaptive) distinguishing sequence we can take $W$ to be a -single suffix, greatly reducing the test suite. Lee and Yannakakis describe an -algorithm in [...] (which we will refer to as the LY algorithm) to efficiently -construct this sequence, if it exists. In our case, most hypotheses did not -enjoy an adaptive distinguishing sequence. In these cases the incomplete result -from the LY algorithm still contained a lot of information which we augmented by -pairwise separating sequences. +In the presence of an (adaptive) distinguishing sequence one can take $W$ to be a +single suffix, greatly reducing the test suite. Lee and Yannakakis \cite{LYa94} describe an +algorithm (which we will refer to as the LY algorithm) to efficiently +construct this sequence, if it exists. In our case, unfortunately, most +hypotheses did not enjoy existence of an adaptive distinguishing sequence. In +these cases the incomplete result from the LY algorithm still contained a lot of +information which we augmented by pairwise separating sequences. + +\begin{figure} + \centering \includegraphics[width=\textwidth]{hyp_20_partial_ds.pdf} + \caption{A small part of an incomplete distinguishing sequence as produced by + the LY algorithm. Leaves contain a set of possible initial states, inner nodes + have input sequences and edges correspond to different output symbols (of + which we only drew some), where Q stands for quiescence.} + \label{fig:distinguishing-sequence} +\end{figure} As an example we show an incomplete adaptive distinguishing sequence for one of -the hypothesis in Figure ??. When we apply the input sequence and observe the right output, we know for sure that the SUL was in -state . Unfortunately not all path lead to a singleton set. When we for -instance apply the sequence and observe the right output, -we know for sure that the SUL was in one of the states . In -these cases we can resort the the pairwise separating sequences. +the hypothesis in Figure~\ref{fig:distinguishing-sequence}. When we apply the +input sequence I46 I6.0 I10 I19 I31.0 I37.3 I9.2 and observe outputs O9 O3.3 Q ... +O28.0, we know for sure that the SUL was in state 788. Unfortunately not all +path lead to a singleton set. When for instance we apply the sequence I46 I6.0 +I10 and observe the outputs O9 O3.14 Q, we know for sure that the SUL was in one +of the states 18, 133, 1287 or 1295. In these cases we have to perform more +experiments and we resort to pairwise separating sequences. We note that this augmented DS-method is in the worst case not any better than the classical Wp-method. In our case, however, it greatly reduced the test suites. Once we have our set of suffixes, which we call $Z$ now, our test algorithm -works as follows. The algorithm first exhaust the set $P I^{\leq k} Z$. If this +works as follows. The algorithm first exhausts the set $P I^{\leq 1} Z$. If this does not provide a counterexample, we will randomly pick test queries from $P I^2 I^\ast Z$, where the algorithm samples uniformly from $P$, $I^2$ and $Z$ (if $Z$ contains more that $1$ sequence for the supposed state) and with a geometric distribution on $I^\ast$. - - -## Subalphabet selection - -During our attempts to learn the ESM we observed that the above method failed to -produce a certain counterexample. With domain knowledge we were able to provide -a handcrafted counterexample which allowed the algorithm to completely learn the -controller. In order to do this automatically we defined a subalphabet which is -important at the initialization phase of the controller. This subalphabet will -be used a bit more often that the full alphabet. We do this as follows. - -We start testing with the alphabet which provided a counterexample for the -previous hypothesis (for the first hypothesis we take the subalphabet). If no -counterexample can be found within a specified query bound, then we repeat with -the next alphabet. If both alphabets do not produce a counterexample within the -bound, the bound is increased by some factor and we repeat all. - -This method only marginally increases the number of tests. But it did find the -right counterexample we first had to construct by hand.