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