Merge branch 'master' of https://github.com/dopefishh/tt2015

[tt2015.git] / a3 / 1modelingTCP.tex

diff --git a/a3/1modelingTCP.tex b/a3/1modelingTCP.tex
index 6449dcc..2c9125b 100644 (file)
--- a/a3/1modelingTCP.tex
+++ b/a3/1modelingTCP.tex
@@ -15,20 +15,33 @@ In this case an LTS, would be a fitting model for our SUT.
 
 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 
+\paragraph{Mealy Machines} 
+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.
+
+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 as described in the TCP specification. 
+SUT transitions through states depending on input as described in the TCP
+specification and produces the output described by 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. 
-
-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
+\subsection{A LTS model of TCP} \label{subsec:sut_model}
+With these model based tests two major parts of the TCP specification will be 
+tested. These are (a) the establishment of connection (three-way handshake)
+between the SUT -which 
+will receive the connection- and an external host -which will initiate the 
+connection- and (b) the closing of a connection (tear down) initiated by the
+external host.
+
+Figure~\ref{fig:model_connection} shows a LTS model of the SUT for the 
+three-way handshake (a). Figure~\ref{fig:model_disconnect} shows a LTS model
+of the SUT for the tear down (b).
+
+Hier zou dus een plaatje van ``digraph Connection'' uit ``graphs.viz'' moeten komen. \label{fig:model_connection}.
+
+En hier een plaatje van ``digraph Close'' uit ``graphs.viz'' moeten komen.
+\label{fig:model_disconnect}
\ No newline at end of file