a3/1modelingTCP.tex

   1 In previous assignments our group has viewed the SUT as a stateful input-output
   2 system.
   3
   4 \subsection{Behaviour of the SUT} \label{subsec:behaviour}
   5 When considering the behaviour of the SUT we abstract away from some details to
   6 limit the scope of the project. We will only consider the behaviour as the
   7 sequence of input output flags. All other details required will be implemented
   8 in the adapter and are invisible to the model. We also do not test erroneous
   9 client behaviour such as dropping packets on purpose or tampering with hashes.
  10 TCP inherently is a state based system and thus we have considered the
  11 following models.
  12
  13 \paragraph{Labeled Transition System (LTS)} A LTS would
  14 be a fitting technique to model the SUT in since the
  15 behaviour of TCP is that both the server and the client have internal states to
  16 which they transition based upon input coming from the other.
  17 Because of this behaviour and the characteristics of LTSs it would be a fitting
  18 technique to model our SUT in.
  19
  20 LTS would not be a compelling choice if we would test tampering with data and
  21 erroneous clients or servers since LTS is purely input output and by default
  22 there is no data involved.
  23
  24 \paragraph{Properties} Describing TCP in terms of properties would in theory
  25 be possible but it would require a very different adapter. The adapter should
  26 be handed a trace and it should run the entire trace and return the sequence of
  27 flags sent and received. Because of the high adapter complexity and the
  28 difficult test generation Properties is not a technique that we consider.
  29
  30 % Ik snap niet waarom mealy en LTS beter of slechter zijn dan elkaar...
  31
  32 %\paragraph{Mealy Machines}
  33 %Mealy Machines are a variant of LTS in which each label is a tuple of input
  34 %and output. This forces each state transition to consume both input and
  35 %produce output. The model for the SUT (see Section~\ref{subsec:sut_model})
  36 %however contains state transitions with sequences of output which do not
  37 %require new input.
  38 %
  39 %Due to this limitation Mealy Machines are not a very suitable model to model
  40 %the SUT. Instead we choose to model the SUT as a LTS. Since LTSs provide the
  41 %functionality to express the desired properties of the SUT, that is, that the
  42 %SUT transitions through states depending on input as described in the TCP
  43 %specification and produces the output described by the TCP specification.
  44
  45 \subsection{A LTS model of TCP}\label{subsec:sut_model}
  46 As said in Section~\ref{subsec:behaviour} we only test the handshake and the
  47 connection termination. These actions are visualized in Figure~\ref{fig:model}.
  48 To touch a little bit of the data transfer we have included with dotted arrows
  49 a hypothetical extra path that depicts data transfer. The \texttt{DAT?} output
  50 label is basically \texttt{ACK} followed by a \texttt{PSH+ACK} including some
  51 random data. The starting state is marked with the number one. The states are
  52 named to match the original RFC the most.
  53
  54 \begin{figure}[H]
  55         \centering
  56         \includegraphics[scale=.75]{lts-jtorx.eps}
  57         \caption{LTS model of the SUT}\label{fig:model}
  58 \end{figure}