An LTS would not be a fitting model in case it would be desirable to model the
behaviour when wrong input (such as wrong sequence numbers) is given to the SUT.
-An LTS could model this behaviour, but more expressive models exists (see below)
-which would limit the size of the model.
-
-In this case we chose to model the SUT as a LTS. Since LTSs provide the
-functionality to express the desired properties of the SUT, that is, that the
-SUT transitions through states as described in the TCP specification.
\paragraph{Mealy Machines}
-Mealy Machines are an extension of LTS in which each label is a tuple of input
-and output. For our SUT this means that is is not just possible to model the
-behaviour of the SUT regarding its internal state, but also its behaviour
-regarding its output.
+Mealy Machines are a variant of LTS in which each label is a tuple of input
+and output. This forces each state transition to consume both input and
+produce output. The model for the SUT (see Section~\ref{subsec:sut_model})
+however contains state transitions with sequences of output which do not
+require new input.
-For simplicity however we have chosen to model the SUT with the assumption that
-it is only handed correct input and will then generate correct output (assuming
-that the internal state transition function is correct). Therefore the extra
-functionality provided by modeling our SUT as a Mealy Machine is not necessary.
\ No newline at end of file
+Due to this limitation Mealy Machines are not a very suitable model to model
+the SUT. Instead we choose to model the SUT as a LTS. Since LTSs provide the
+functionality to express the desired properties of the SUT, that is, that the
+SUT transitions through states depending on input as described in the TCP
+specification and produces the output described by the TCP specification.
\ No newline at end of file
repositories / tt2015.git / commitdiff