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}
   5 When considering the behaviour of the SUT we will only consider it's behaviour
   6 with regards to correct input and output. In this case some models are more
   7 fitting than others.
   8
   9 \paragraph{Labeled Transition System} A Labeled Transition System (LTS) would
  10 be a fitting model for our SUT as the
  11 behaviour of TCP is such that a TCP client is in a certain state (connection
  12 closed, listening, connection established, etc.) and the TCP client transitions
  13 between those states based upon input coming from another connected client.
  14 In this case an LTS, would be a fitting model for our SUT.
  15
  16 An LTS would not be a fitting model in case it would be desirable to model the
  17 behaviour when wrong input (such as wrong sequence numbers) is given to the SUT.
  18
  19 \paragraph{Mealy Machines}
  20 Mealy Machines are a variant of LTS in which each label is a tuple of input
  21 and output. This forces each state transition to consume both input and
  22 produce output. The model for the SUT (see Section~\ref{subsec:sut_model})
  23 however contains state transitions with sequences of output which do not
  24 require new input.
  25
  26 Due to this limitation Mealy Machines are not a very suitable model to model
  27 the SUT. Instead we choose to model the SUT as a LTS. Since LTSs provide the
  28 functionality to express the desired properties of the SUT, that is, that the
  29 SUT transitions through states depending on input as described in the TCP
  30 specification and produces the output described by the TCP specification.
  31
  32 \subsection{A LTS model of TCP} \label{subsec:sut_model}
  33 With these model based tests two major parts of the TCP specification will be
  34 tested. These are (a) the establishment of connection (three-way handshake)
  35 between the SUT -which
  36 will receive the connection- and an external host -which will initiate the
  37 connection- and (b) the closing of a connection (tear down) initiated by the
  38 external host.
  39
  40 Figure~\ref{fig:model_connection} shows the LTS model of the SUT.
  41
  42 \begin{figure}[H]
  43         \centering
  44         \includegraphics[scale=.75]{lts-jtorx.eps}
  45         \caption{LTS system}\label{fig:model}
  46 \end{figure}