+++ /dev/null
-% Comparison between tools and how fit the tools we choose were
-
-% Discuss and classify the MBT tools that you used, compare them, compare with
-% Manual testing, and reflect on the theory:
-% • What is implementation relation?
-% • Is there support for non-determinism, concurrency?
-% • Are the generated tests sound, exhaustive? Why do you think so?
-% • Which method of test test selection is used?
-% • What is the modeling notation, its expressiveness, and ease of use?
-% • Do the tools use on/off-line testing (on-the-fly/batch)?
-% • Do they support both: test input generation and output checking?
-
-The SUT has been tested using two tools, JTorX and \GAST. Both tools allowed
-for extensive testing of the SUT compared to the model of
-Section~\ref{sec:modeling} using the architecture of Figure~\ref{fig:arch}.
-
-However setting up both \GAST and JTorX required extensive effort. To be able
-to use \GAST extensive changes had to be made to the source code of \GAST.
-Without these changes \GAST could not be used effectively. This was due in
-part to problems with Cleans uniqueness typing when using \GAST over TCP. The
-complete list of changes can be obtained by comparing \GAST s source code to the
-source code found in the attached \texttt{code/Gast/} folder.
-
-\GAST selects tests by trying all inputs from the alphabet in each possible
-state. When the SUT responds in a way which is not in the model the test case
-fails. JTorX selects test cases by ???????????????
-\GAST s selection ensures that all possible traces are covered, however, this
-exhaustive search will also generate huge tests for big models.
-
-% hier iets over non-determinism?
-
-Both JTorX and \GAST use on-line checking. They test the SUT on the fly by
-syncing state transitions in the internal model of the SUT with observed output (after input) from the SUT.
-
-For JTorX test generation was very simple since it accepts models in GraphViz
-DOT language, which is also the language used for describing the models for this
-report. For \GAST the model generation required a bit more work, as the model
-is written as a function in Clean. This translation is however easily done by
-hand. Because the model for \GAST is written as a function in Clean it is very
-expressive, the modeling method chosen for JTorX however is a lot less
-expressive, as it just allows for specification of states and transition labels
-between them. However JTorX allows for many different modeling languages, which
-can be more expressive than modeling using GraphViz models \cite{JTorXSite}.
-However, for our tests GraphViz models were expressive enough.
\ No newline at end of file
repositories / tt2015.git / blobdiff