system.
\subsection{Behaviour of the SUT}
-When considering the behaviour of the SUT we will only consider it's behaviour
-with regards to correct input and output. In this case some models are more
-fitting than others.
-
-\paragraph{Labeled Transition System} A Labeled Transition System (LTS) would
-be a fitting model for our SUT as the
-behaviour of TCP is such that a TCP client is in a certain state (connection
-closed, listening, connection established, etc.) and the TCP client transitions
-between those states based upon input coming from another connected client.
-In this case an LTS, would be a fitting model for our SUT.
-
-An LTS would not be a fitting model in case it would be desirable to model the
-behaviour when wrong input (such as wrong sequence numbers) is given to the SUT.
-
-\paragraph{Mealy Machines}
-Mealy Machines are a variant of LTS in which each label is a tuple of input
-and output. This forces each state transition to consume both input and
-produce output. The model for the SUT (see Section~\ref{subsec:sut_model})
-however contains state transitions with sequences of output which do not
-require new input.
-
-Due to this limitation Mealy Machines are not a very suitable model to model
-the SUT. Instead we choose to model the SUT as a LTS. Since LTSs provide the
-functionality to express the desired properties of the SUT, that is, that the
-SUT transitions through states depending on input as described in the TCP
-specification and produces the output described by the TCP specification.
-
-\subsection{A LTS model of TCP} \label{subsec:sut_model}
-With these model based tests two major parts of the TCP specification will be
-tested. These are (a) the establishment of connection (three-way handshake)
-between the SUT -which
-will receive the connection- and an external host -which will initiate the
-connection- and (b) the closing of a connection (tear down) initiated by the
-external host.
-
-Figure~\ref{fig:model_connection} shows the LTS model of the SUT.
+When considering the behaviour of the SUT we abstract away from some details to
+limit the scope of the project. We will only consider the behaviour as the
+sequence of input output flags. All other details required will be implemented
+in the adapter and are invisible to the model. We also do not test erroneous
+client behaviour such as dropping packets on purpose or tampering with hashes.
+TCP inherently is a state based system and thus we have considered the
+following models.
+
+\paragraph{Labeled Transition System (LTS)}. A LTS would
+be a fitting technique to model the SUT in since the
+behaviour of TCP is that both the server and the client have internal states to
+which they transition based upon input coming from the other.
+Because of this behaviour and the characteristics of LTSs it would be a fitting
+technique to model our SUT in.
+
+LTS would not be a compelling choice if we would test tampering with data and
+erroneous clients or servers since LTS is purely input output and by default
+there is no data involved.
+
+\paragraph{Properties}. Describing TCP in terms of properties would in theory
+be possible but it would require a very different adapter. The adapter should
+be handed a trace and it should run the entire trace and return the sequence of
+flags sent and received. Because of the high adapter complexity and the
+difficult test generation Properties is not a technique that we consider.
+
+% Ik snap niet waarom mealy en LTS beter of slechter zijn dan elkaar...
+
+%\paragraph{Mealy Machines}
+%Mealy Machines are a variant of LTS in which each label is a tuple of input
+%and output. This forces each state transition to consume both input and
+%produce output. The model for the SUT (see Section~\ref{subsec:sut_model})
+%however contains state transitions with sequences of output which do not
+%require new input.
+%
+%Due to this limitation Mealy Machines are not a very suitable model to model
+%the SUT. Instead we choose to model the SUT as a LTS. Since LTSs provide the
+%functionality to express the desired properties of the SUT, that is, that the
+%SUT transitions through states depending on input as described in the TCP
+%specification and produces the output described by the TCP specification.
+
+\subsection{A LTS model of TCP}\label{subsec:sut_model}
+As said in Section~\ref{subsec:behaviour} we only test the handshake and the
+connection termination. These actions are visualized in Figure~\ref{fig:model}.
+To touch a little bit of the data transfer we have included with dotted arrows
+a hypothetical extra path that depicts data transfer. The \texttt{DAT?} output
+label is basically \texttt{ACK} followed by a \texttt{PSH+ACK} including some
+random data. The starting state is marked with the number one. The states are
+named to match the original RFC the most.
\begin{figure}[H]
\centering
\includegraphics[scale=.75]{lts-jtorx.eps}
- \caption{LTS system}\label{fig:model}
+ \caption{LTS model of the SUT}\label{fig:model}
\end{figure}
% argue why you selected these
% tools. (See also the list of MBT tools below.)
-To test the TCP model of Section~\ref{sec:modeling} two tools have been
-considered. \GAST and JTorx. The sections below discuss the upsides and
-downsides of these tools in regard to testing the SUT.
+To test the SUT using the model from Section~\ref{sec:modeling} we have
+considered two tools, namely \GAST and JTorx. The sections below discuss the
+upsides and downsides of these tools in regard to testing the SUT.
-\subsection{JTorx of Graphwalker ofzo}
+\subsection{JTorX}
+JTorX is an open source model based test tool developed by
+Belinfante\cite{belinfante2010jtorx} featuring a GUI, all possible graph file
+formats and can connect to the SUT via TCP or stdin/stdout. JTorX generates
+input enabled traces and automatically executes them via the adapter. In our
+setup we use TCP as the desired communication method between the SUT and the
+tool.
-\subsection{\GAST}
\ No newline at end of file
+\subsection{\GAST}
+\GAST is an open source model based test tool developed by Koopman et
+al.\cite{koopman2003gast} and is a design specific language written in the
+functional programming language Clean. Models in \GAST must be expressed as
+functions. \GAST supports two different types of testing. Standard model
+checking and property based testing. As discussed earlier we are not using
+property based testing. \GAST can communicate with the SUT via TCP or embedded
+C code. In our setup we use TCP as the desired communication method between the
+SUT and the tool.
+
+% Misschien hier iets over het feit dat we TCP gebruiken als communicatie
repositories / tt2015.git / commitdiff