From: Mart Lubbers Date: Sun, 20 Dec 2015 18:18:47 +0000 (+0100) Subject: update hfst 1 2 X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=af2a9cb5d392889d4b6745a002e73cacd55112ec;p=tt2015.git update hfst 1 2 --- diff --git a/a3/1modelingTCP.tex b/a3/1modelingTCP.tex index 6846389..0db7faf 100644 --- a/a3/1modelingTCP.tex +++ b/a3/1modelingTCP.tex @@ -2,45 +2,57 @@ In previous assignments our group has viewed the SUT as a stateful input-output system. \subsection{Behaviour of the SUT} -When considering the behaviour of the SUT we will only consider it's behaviour -with regards to correct input and output. In this case some models are more -fitting than others. - -\paragraph{Labeled Transition System} A Labeled Transition System (LTS) would -be a fitting model for our SUT as the -behaviour of TCP is such that a TCP client is in a certain state (connection -closed, listening, connection established, etc.) and the TCP client transitions -between those states based upon input coming from another connected client. -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. - -\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} -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 the LTS model of the SUT. +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 system}\label{fig:model} + \caption{LTS model of the SUT}\label{fig:model} \end{figure} diff --git a/a3/2tools.tex b/a3/2tools.tex index 22dd196..03e7f8d 100644 --- a/a3/2tools.tex +++ b/a3/2tools.tex @@ -4,10 +4,26 @@ % argue why you selected these % tools. (See also the list of MBT tools below.) -To test the TCP model of Section~\ref{sec:modeling} two tools have been -considered. \GAST and JTorx. The sections below discuss the upsides and -downsides of these tools in regard to testing the SUT. +To test the SUT using the model from Section~\ref{sec:modeling} we have +considered two tools, namely \GAST and JTorx. The sections below discuss the +upsides and downsides of these tools in regard to testing the SUT. -\subsection{JTorx of Graphwalker ofzo} +\subsection{JTorX} +JTorX is an open source model based test tool developed by +Belinfante\cite{belinfante2010jtorx} featuring a GUI, all possible graph file +formats and can connect to the SUT via TCP or stdin/stdout. JTorX generates +input enabled traces and automatically executes them via the adapter. In our +setup we use TCP as the desired communication method between the SUT and the +tool. -\subsection{\GAST} \ No newline at end of file +\subsection{\GAST} +\GAST is an open source model based test tool developed by Koopman et +al.\cite{koopman2003gast} and is a design specific language written in the +functional programming language Clean. Models in \GAST must be expressed as +functions. \GAST supports two different types of testing. Standard model +checking and property based testing. As discussed earlier we are not using +property based testing. \GAST can communicate with the SUT via TCP or embedded +C code. In our setup we use TCP as the desired communication method between the +SUT and the tool. + +% Misschien hier iets over het feit dat we TCP gebruiken als communicatie diff --git a/a3/tt3.bib b/a3/tt3.bib index 2a937c4..28a90fc 100644 --- a/a3/tt3.bib +++ b/a3/tt3.bib @@ -59,3 +59,23 @@ Updated by RFCs 1122, 3168, 6093, 6528}, year = {2000}, pages = {70--79}, } +@incollection{belinfante2010jtorx, + title={JTorX: A tool for on-line model-driven test derivation and + execution}, + author={Belinfante, Axel}, + booktitle={Tools and Algorithms for the Construction and Analysis + of Systems}, + pages={266--270}, + year={2010}, + publisher={Springer} +} +@incollection{koopman2003gast, + title={Gast: Generic automated software testing}, + author={Koopman, Pieter and Alimarine, Artem and Tretmans, Jan and + Plasmeijer, Rinus}, + booktitle={Implementation of Functional Languages}, + pages={84--100}, + year={2003}, + publisher={Springer} +} + diff --git a/a3/tt3.tex b/a3/tt3.tex index c4c8e4f..bbf776f 100644 --- a/a3/tt3.tex +++ b/a3/tt3.tex @@ -20,6 +20,6 @@ \input{5discussion.tex} %\nocite{*} %% weghalen bij daadwerkelijke cite -%\bibliographystyle{plain} -%\bibliography{tt2} +\bibliographystyle{ieeetr} +\bibliography{tt3} \end{document}