JTorX - a tool for Model-Based Testing

What?

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.

Extensions to JTorX have been contributed by David Farago and Felix Kutzner.
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:

Features

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).

Overview:

Aldebaran (.aut) built-in
GraphML (.graphml) built-in
GraphViz (.dot,.gv) built-in
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.

Screenshots

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);
    1. just load two .aut or .graphml files (thanks Lars :-)
    2. indicate the implementation kind (model, directly connected)
    3. optionally, load a test purpose file, and enable toggle guide
    4. 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.
    5. specify whether Straces or Utraces should be used
    6. select the Test pane in the bottom part of the window
    7. 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.

Usage scenarios

see: Usage scenarios

Downloads

  • software packages for windows, linux and mac (os x 10.[45]): 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

There is an 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

Dependencies

  • java 1.5

Platform dependencies

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:

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

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).

License

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
met:

  • 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.

Links

Publications

PhD Thesis

Description of Tool

Underlying Theory

Case Studies

Other References

see List of References (under construction).

Portfolio

Portfolio of cases where JTorX has been used (under construction).

Acknowledgements

Contact

Notes

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.

main.pdf - JTorX: a Tool for On-Line Model-Driven Test Derivation and Execution (103 KB) Axel Belinfante, 15 Jan 2010 21:32

fmics2011.pdf (340 KB) Axel Belinfante, 29 Sep 2011 17:08

mbtlts.pdf (387 KB) Axel Belinfante, 29 May 2015 00:47