somme ex2 and ex3 text

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

diff --git a/a3/1modelingTCP.tex b/a3/1modelingTCP.tex
deleted file mode 100644 (file)
index 10e4110..0000000
--- a/a3/1modelingTCP.tex
+++ /dev/null
@@ -1,58 +0,0 @@
-In previous assignments our group has viewed the SUT as a stateful input-output
-system. 
-
-\subsection{Behaviour of the SUT} \label{subsec:behaviour}
-When considering the behaviour of the SUT we abstract away from some details to
-limit the scope of the project. We will only consider the behaviour as the
-sequence of input output flags. All other details required will be implemented
-in the adapter and are invisible to the model. We also do not test erroneous
-client behaviour such as dropping packets on purpose or tampering with hashes.
-TCP inherently is a state based system and thus we have considered the
-following models.
-
-\paragraph{Labeled Transition System (LTS)} A LTS would 
-be a fitting technique to model the SUT in since the 
-behaviour of TCP is that both the server and the client have internal states to
-which they transition based upon input coming from the other.
-Because of this behaviour and the characteristics of LTSs it would be a fitting
-technique to model our SUT in.
-
-LTS would not be a compelling choice if we would test tampering with data and
-erroneous clients or servers since LTS is purely input output and by default
-there is no data involved.
-
-\paragraph{Properties} Describing TCP in terms of properties would in theory
-be possible but it would require a very different adapter. The adapter should
-be handed a trace and it should run the entire trace and return the sequence of
-flags sent and received. Because of the high adapter complexity and the
-difficult test generation Properties is not a technique that we consider.
-
-% Ik snap niet waarom mealy en LTS beter of slechter zijn dan elkaar...
-
-%\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 depending on input as described in the TCP
-%specification and produces the output described by the TCP specification.
-
-\subsection{A LTS model of TCP}\label{subsec:sut_model}
-As said in Section~\ref{subsec:behaviour} we only test the handshake and the
-connection termination. These actions are visualized in Figure~\ref{fig:model}.
-To touch a little bit of the data transfer we have included with dotted arrows
-a hypothetical extra path that depicts data transfer. The \texttt{DAT?} output
-label is basically \texttt{ACK} followed by a \texttt{PSH+ACK} including some
-random data. The starting state is marked with the number one. The states are
-named to match the original RFC the most.
-
-\begin{figure}[H]
-       \centering
-       \includegraphics[scale=.75]{lts-jtorx.eps}
-       \caption{LTS model of the SUT}\label{fig:model}
-\end{figure}