JTorX - a tool for Model-Based Testing¶
- JTorX - a tool for Model-Based Testing
- What is its status?
- How can it be run?
JTorX is a tool to test whether the ioco testing relation holds between a given specification and a given implementation.
It can do so for Straces and Utraces of the specification.
The specification is given as Labelled Transition System (LTS) - represented for example in Aldebaran (.aut) or GraphML (.graphml) format,
or as Symbolic Transition System (STS).
The implementation is either also given as LTS, or it is given as a real program, in which case JTorX will need to be able to interact with it.
JTorX is out-of-the-box able to interact with programs that communicate on their standard input and output, or via tcp, using the same labels as in the specification.
For other programs an adapter has to be given.
JTorX is able to use adapter programs that have been developed for TorX.
JTorX is a reimplementation of the core functionality of TorX in Java -- with additional features added.
Compared to TorX, JTorX is based on more modern theory, and JTorX is much easier to deploy (regarding both installation and use).
From version 1.10 beta on, JTorX can be used both with a GUI (graphical user interface), and without a GUI (from the command line, or from scripts). (Earlier version can only be run via a GUI).
Please refer to the paper Model Based Testing with Labelled Transition Systems (mbtlts.pdf, pdf) by Jan Tretmans for a detailed elaboration of the theory.
The paper JTorX: a Tool for On-Line Model-Driven Test Derivation and Execution, main.pdf, describes the tool, as does the PhD thesis JTorX: Exploring Model-Based Testing.
What is its status?¶
The current version has been successfully used in our testing techniques course,
and in an internship where it found bugs that otherwise probably wouldn't have been found.
Nevertheless, it is still work in progress in the sense that it is regularly extended.
They have built on the support for STS (symbolic transition system) models that was originally developed by Lars Frantzen.
These extensions are currently not integrated in the JTorX version available via the downloads section on this page, but the extensions are available as separate branches in the following repositories:
Like TorX, JTorX accesses a model on-the-fly: it only accesses that part of the model that is necessary to compute the next test step; this allows testing with models that have an infinite state space1.
JTorX supports the use of guidance (test purposes) to guide (steer) the test derivation
The test purpose must either be an automaton, in which the success state(s) in which the test purpose is reached is marked by a self-loop transition with label
epsilon, or an LTS in which all end (sink) states are success states.
Supported Modeling Formalisms¶
JTorX contains built-in support for models given in Aldebaran (.aut), GraphML (.graphml) or GraphViz (.dot,.gv) format.
JTorX supports the use of existing TorX explorers (including symbolic features, i.e. the use of labels with variables) to access models.
The support for parameterized transition systems, where the labels contain variables (with constraints over them) is used for timed testing with uppaal-style models, and for testing with STSes (Symbolic Transition Systems). There is no support (yet) to use guidance (test purposes) with parameterized transition systems.
Existing TorX explorers can be used to access muCRL or mCRL2 models, e.g. via ltsmin, to use Jararaca to describe test purposes, to use ta2torx to access an uppaal-style model that consists of a network of timed automata, and to access models via the CADP open-caesar interface. Support for Jararaca is included in the JTorX distribution; support for muCRL or mCRL2 models is distributed with the mCRL2 and LTSmin toolkits; support for access to models via the CADP open-caesar interface is distributed with TorX (we are currently studying how to distribute this with JTorX).
|Jararaca (regular-expression based language designed to describe test-purposes)(.jrrc)||built-in (via language module distributed with JTorX)|
|Symbolic Transition System (.sax)||built-in (via language module distributed with JTorX)|
|muCRL, mCRL2||for infinite models: via lps2torx distributed with mCRL2 toolset and with LTSmin|
|muCRL, mCRL2||for finite models: by translation of model to .aut and using built-in .aut support|
|Binary Coded Graphs (.bcg)||via cadp support distributed with TorX|
|LOTOS||via cadp support distributed with TorX|
|other formalisms accessed via CADP open/caesar interface||via cadp support distributed with TorX|
Connecting to System Under Test¶
JTorX contains built-in adapters for programs that communicate on their standard input and output, or via tcp, using the same labels as in the specification.
JTorX supports the use of existing TorX adapters2. Compared to TorX this interface has been extended to be able to deal with output from the system under test that is received while the tester wanted to apply a stimulus.
The built-in adapter for programs that communicate on their standard input and output, and the torx-adapter interface support timed testing.
Other Features¶JTorX contains features not found in TorX:
- It derives test-cases that are input-enabled (i.e. that are always ready to accept output from the system under test)
- Support for testing with Utraces (in addition to Straces) has been added in 0.999.
- iocoChecker, a tool (developed by Lars Frantzen) to check whether two models are ioco-related, has been integrated (loosely, for now).
- A checker is included that (for finite state systems) can check whether the Straces coincide with the Utraces.
- Simulation functionality is included. The simulation can be guided, e.g. using the log of a test run.
Some screenshots are available on a separate page (warning: there are quite a few of them, and they are not small, and they are made with a JTorX version that is now a bit old).
How can it be run?¶JTorX is relatively easy to deploy, on Unix (binary download available for Linux), Windows, and Mac:
- download and unpack (see below)
- execute jtorx (for linux) or jtorx.bat (on windows) from within the jtorx* folder that results from unpacking the distribution, or just run the JTorX app (on a mac)
- no configuration (this has to be worked on);
- just load two .aut or .graphml files (thanks Lars :-)
- indicate the implementation kind (
model, directly connected)
- optionally, load a test purpose file, and enable toggle guide
- specify what inputs/outputs are (Interpretation in the gui)
- prefix with ! and ?,
- postfix with ! and ?, or
- give a list of input action names and a list of output action names.
- specify whether
Utracesshould be used
- select the
Testpane in the bottom part of the window
- click on start
Note: transitions labelled with i or tau in Aldebaran (.aut) and GraphML (.graphml) files are interpreted as internal (non-observable) transitions.
(The same typically holds for labels of which the first word is i or tau)
When models are accessed via the TorX explorer interface (ltsmin, muCRL, mCRL2, jararaca), the conventions of the corresponding formalism are used w.r.t. observable v.s. non-observable transitions.
Note: a lot of debugging output will appear on stdout/stderr.
Note: the automata visualization does not work on ppc mac.
Note: after downloading and unpacking you can move around the jtorx* directory that results from unpacking, but the files in it should be next to each other, otherwise the application (jar_ nr .jar) can not find its support files.
see: Usage scenarios
- software packages for windows, linux and mac (os x 10.): in the files section
- source code: browsable (git) repository
- examples: the files section contains coffee examples of TorX (jtorx-ex.tgz) and examples from the iocoChecker distribution
- java 1.5
The provided software downloads are platform specific.
There is one additional dependency for Mac OS X 10.8 (Mountain Lion), for the anidot automaton visualization. No longer necessary, see anidot visualization updated for Mac OS X (Mountain) Lion
Platform dependencies in general functionality of JTorX¶
JTorX downloads contain platform specific versions of the following general files:
- swt.jar, for the swt based graphical user interface, and
- tclkit, for the animation viewers (legacy TorX)
JTorX packages for other platforms can be produced from the jtorx package for linux, by replacing these two files by versions for your platform.
For many platforms, precompiled versions of these files are available:
- swt.jar, at http://download.eclipse.org/eclipse/downloads/drops/R-3.4-200806172000/index.php
- tclkit, at http://www.equi4.com/tclkit/download.html
Platform dependencies in support for specific model formalisms¶
JTorX downloads contains platform specific versions of the following programs
- jararaca, the TorX-explorer component for the jaraca language in which we can describe traces using regular expressions
- treeSolver, the constraint solver that is used when we use an STS as model
Without these programs JTorX can still be used with other modeling formalisms.
Feedback is appreciated. Issues can be reported via this tracker (you need to register yourself first), or directly via email (see Contact, at the end).
Copyright (c) 2009-2011, Formal Methods and Tools, University of Twente
All rights reserved.
Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are
- Redistributions of source code must retain the above copyright
notice, this list of conditions and the following disclaimer.
- Redistributions in binary form must reproduce the above copyright
notice, this list of conditions and the following disclaimer in the
documentation and/or other materials provided with the distribution.
- Neither the name of the University of Twente nor the names of its
contributors may be used to endorse or promote products derived from
this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
- Axel Belinfante JTorX: Exploring Model-Based Testing. PhD thesis, University of Twente. CTIT Ph.D.-thesis series No. 14-319 ISBN 978-90-365-3707-0 (2014)
Description of Tool¶
- Axel Belinfante. JTorX: a Tool for On-Line Model-Driven Test Derivation and Execution. In: Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010. LNCS vol. 6015, pp. 266-270. Springer. main.pdf (2010)
- Jan Tretmans and Ed Brinksma. TorX: Automated Model-Based Testing. In: First European Conference on Model-Driven Software Engineering, December 11-12, 2003, Nuremberg, Germany. pp. 31-43. (2003)
- Jan Tretmans. Model Based Testing with Labelled Transition Systems. In: Formal Methods and Testing. LNCS, vol. 4949, pp. 1-38. Springer (2008) (mbtlts.pdf , pdf)
- Marten Sijtema, Marielle I.A. Stoelinga, Axel Belinfante, and Lawrence Marinelli. Experiences with Formal Engineering: Model-Based Specification, Implementation and Testing of a Software Bus at Neopost, FMICS 2011. LNCS vol. 6959, pp. 117-133. Springer. fmics2011.pdf (2011)
see List of References (under construction).
Portfolio of cases where JTorX has been used (under construction).
- initial graphml parsing code was derived from Lars Frantzen's code in iocoChecker
- icon by André Nijmeijer
- SWTLoader by Silvio Moioli
- iocoChecker by Lars Frantzen
- Apache Commons exec
- initial tkdock, windowlist and mactoolbar code by Kevin Walzer. The initial code has been changed for use in animators AniDot and AniMsc: tkdock has been extended to be usable in starkit, and windowlist and mactoolbar have been modified to work on non-macos systems. In addition, windowlist has been extended to show (checkmark, diamond) icons next to the menu entries, and to also list iconified windows.
1 As long as each state has a finite number of outgoing transitions. With TorX we once compared a LOTOS model with an mCRL2 model of the same system, where both models had an infinite state space (due to un-bounded buffers that were part of the models), and found an (unintended) error. We have not repeated that experiment with JTorX, but it is rather easy to do so.
2 We use the word adapter to refer to the glue-code that is used to connect JTorX to a particular system that is to be tested.