In previous assignments our group has viewed the SUT as a stateful input-output
system. 

\subsection{Behaviour 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 model of the SUT}\label{fig:model}
\end{figure}
