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, would be a fitting model for our SUT.
  16
  17 An LTS would not be a fitting model in case it would be desirable to model the
  18 behaviour when wrong input (such as wrong sequence numbers) is given to the SUT.
  19 An LTS could model this behaviour, but more expressive models exists (see below)
  20 which would limit the size of the model.
  21
  22 In this case we chose to model the SUT as a LTS. Since LTSs provide the
  23 functionality to express the desired properties of the SUT, that is, that the
  24 SUT transitions through states as described in the TCP specification.
  25
  26 \paragraph{Mealy Machines}
  27 Mealy Machines are an extension of LTS in which each label is a tuple of input
  28 and output. For our SUT this means that is is not just possible to model the
  29 behaviour of the SUT regarding its internal state, but also its behaviour
  30 regarding its output.
  31
  32 For simplicity however we have chosen to model the SUT with the assumption that
  33 it is only handed correct input and will then generate correct output (assuming
  34 that the internal state transition function is correct). Therefore the extra
  35 functionality provided by modeling our SUT as a Mealy Machine is not necessary.