1 % testcases, results and discussion on results:
3 % Write your model in the input language of the selected MBT tools, generate
5 % them on your SUT. Explain your observations and analyse the test results.
8 The model in itself was usable in JTorX since the model was written in
9 Graphviz' DOT language which is readable by JTorX. JTorX itself generates all
10 the testcases and after over $
8000$ state changes we stopped the testing. There
11 are an infinite number of traces possible because there are several loops in
12 the model. The logfile generated by JTorX is $
6.7MB$ long and contains indepth
13 detail about the trace.
15 \begin{lstlisting
}[caption=
{Last lines of JTorX' log saying the sut has passed
}]
16 2015-
12-
20T21:
17:
32.370+
0100 VERDICT
8500 pass
17 2015-
12-
20T21:
17:
32.370+
0100 EOT
8500
18 2015-
12-
20T21:
17:
32.371+
0100 LOG
8500 (tcpclient-label-Adapter) streamreader io exception: Socket closed
22 \GAST requires an input enabled model, therefore the actual specification is a
23 bit different compared to the other tools. This model, generated by
\GAST can be
24 seen in Figure~
\ref{fig:model
}.
28 \includegraphics[scale=
.75]{gast.eps
}
29 \caption{Model generated by
\GAST}\label{fig:model
}
32 The
\texttt{ConnectionError
} state is added to make the model input enabled.
33 All inputs (packets sent from
\emph{SUT
}) which the original TCP specification
34 deems illegal in a given state are redirected to this state which is also
35 defined as one of the final states together with
\emph{Closed
}.
36 When
\GAST will end up in this state the SUT is reset and a new path is tried.
38 Because of time constraints we decided to allow
\GAST to evaluate $
9000$ paths.
39 None of the paths where rejected by
\GAST. The output generated by
\GAST is
42 \begin{lstlisting
}[caption=
{Gast commandline output
}]
44 paths:
8999, rejected:
0, truncated:
0...
45 End of testing, maximum paths used.
46 9000 test paths executed successful, in total
12252 transitions.