Tools - iocoChecker


Memberships

Activities

Teaching

Tools - iocoChecker

Publications

New Homepage!

iocoChecker has become a part of the Model-Based Testing Tool JTorX:

http://fmt.cs.utwente.nl/redmine/wiki/jtorx/

The remainder of this page is outdated! You can still use this stand-alone version, but it is no longer maintained.


iocoChecker is a Java tool to verify if the ioco testing relation holds between a specification and an implementation Labelled Transition System (LTS). It can do so for Straces and Utraces of the specification. Please refer to the paper Model Based Testing with Labelled Transition Systems by Jan Tretmans for a detailed elaboration of the theory.

The LTSs can be modelled either with the yEd Java Graph Editor, or be given in the Aldebaran .aut textual format. The following two pictures show each an LTS modelled with the yEd editor:

    

If you use the editor take care that:

  • there is exactly one state with label '1' (this marks the initial state)

  • input labels start with a question mark '?', like '?button'

  • output labels start with an exclamation mark '!', like '!chocolate'

  • unobservable transitions have the label 'tau'

  • the LTS is convergent, meaning it does not have tau-loops

  • the graph is saved in the normal yEd yFiles Graph format (*.graphml)

If you use the Aldebaran format take care that:

  • input labels start with a question mark '?', like '?button'

  • output labels start with an exclamation mark '!', like '!chocolate'

  • unobservable transitions have the label 'tau' or 'i'

  • the LTS is convergent, meaning it does not have tau-loops

  • the file-name extension is '.aut'

iocoChecker will check if the implementation LTS is input enabled. If this is not the case, it will add self-loops at all stable states such that they become input enabled (a stable state is a state not having an outgoing unobservable transition). For instance, the right LTS shown above is input enabled, the left one is not. If you choose the left one as being the implementation LTS, iocoChecker will add self-loops with label '?button' at states 2,4,5, and 6.


The download archive contains the iocoChecker.jar. Depending on your settings you can start it by just double-clicking it, or invoke on a command-line:

java -jar iocoChecker.jar

Note that this will also provide you with some debugging information on the console. Now point iocoChecker to the GraphML or Aldebaran files, choose the Straces or the Utraces, and click "Check!". It either proves the relation, or gives all shortest suspension traces which show that ioco does not hold.


 


By a
shortest suspension trace we mean the following: if several suspension traces lead to the same states of the specification and of the implementation, iocoChecker will only report the shortest one. If, for instance, for all traces:
?a
?a ?a !b ?a
?a ?a !b ?a ?a !b ?a
...
in general:
?a (?a !b ?a)*
holds that the same specification and implementation states are reached, iocoChecker will only report the ?a trace.

To run the iocoChecker, a Java runtime environment version 5 or greater is needed. Thanks to GIMP for the logo. Please send questions, comments, improvements, etc., to lars AT frantzen DOT info.

iocoChecker is licensed under the GNU General Public License Version 3.


Download

Current Version: 061108

New
in this version:

  • The checking algorithm is not recursive anymore.

  • If the implementation LTS is not input enabled, iocoChecker now makes it so by adding self-loop transitions at all stable states which are not input enabled.

  • iocoChecker can now directly read Aldebaran .aut files, the awk script (which had some bugs) is not longer necessary to do the conversion.

The .jar contains the sources.

iocoChecker061108_Java6.zip (for Java >= 6)
iocoChecker061108_Java5.zip (for Java >= 5)


Last changed: 09/10/201018:43:32