a3/1modelinvestigation.tex

   1 \section{Modeling TCP}
   2 In previous assignments our group has viewed the SUT as a stateful input-output
   3 system.
   4
   5 \subsection{Behaviour of the SUT}
   6 When considering the behaviour of the SUT we will only consider it's behaviour
   7 with regards to correct input and output. In this case some models are more
   8 fitting than others.
   9
  10 \paragraph{Labeled Transition System} A Labeled Transition System (LTS) would
  11 be a fitting model for our SUT as the
  12 behaviour of TCP is such that a TCP client is in a certain state (connection
  13 closed, listening, connection established, etc.) and the TCP client transitions
  14 between those states based upon input coming from another connected client.
  15 In this case an LTS, in which the interactions would be initiated by the
  16 remote client, would be a fitting model for our SUT.
  17
  18 An LTS would not be a fitting model in case it would be desirable to model the
  19 behaviour when wrong input (such as wrong sequence numbers) is given to the SUT.
  20
  21 \paragraph{Mealy Machines}
  22 Mealy Machines are an extension of LTS in which each label is a tuple of input
  23 and output. For our SUT this means that is is not just possible to model the
  24 behaviour of the SUT regarding its internal state, but also its behaviour
  25 regarding its output.
  26
  27 For simplicity however we have chosen to model the SUT with the assumption that
  28 it is only handed correct input and will then generate correct output (assuming
  29 that the internal state transition function is correct). Therefore the extra
  30 functionality provided by modeling our SUT as a Mealy Machine is not necessary.