I7 Logo
Chair for Foundations of Software Reliability and Theoretical Computer Science
Informatik Logo TUM Logo
jMoped 2.0

Overview

jMoped is a test environment for Java programs written as an Eclipse plug-in.

Given a Java method, jMoped can simulate the execution of the program for all possible arguments within a finite range and generate coverage information for these executions. Moreover, it checks for some common Java errors, i.e. assertion violations, null pointer exceptions, and array bound violations. When an error is found, jMoped finds out the arguments that lead to the error. A JUnit test case can also be automatically generated for further testing.


News

25.09.2008: jMoped 2.0.2 is released. The update includes several bug fixes and an improved version of the reachability algorithm. In essence, when computing successor states, the algorithm ignores the states in which their successors are already discovered. For this, we introduce a new difference operator to make sure that no states are considered twice. This results in significant speed-ups in many experiments.

02.07.2008: A small bug fix in the command-line translator.

04.06.2008: jMoped 2.0.1 is released. The update involves several bug fixes concerning annotations and type conversions.

10.04.2008: jMoped 2.0 is released. The code has been overhauled since the release of jMoped 1.0. It's now faster, more stable, and supports many new features including multithreaded programs, floating numbers, and multiple counterexamples. We are now using JavaBDD for manipulating BDDs in the back-end, which enables jMoped to run on Linux, Mac OS X, and Windows machines. The installation process is also much easier than in version 1.0.


Screenshots Not Covered Partially Covered Covered Assertion Violation Not Enough Heap NullPointerException ArrayIndexOutOfBoundException

See some screenshots of jMoped testing a quicksort implementation.

Requirements

  • Java 5.0 or later
  • Eclipse 3.3 or later
  • JUnit 4 or later

Download & Installation

  1. Eclipse plug-in
    • Inside Eclipse, select Help -> Software Updates -> Find and Install....
    • Select the checkbox Search for new features and install and click the Next button.
    • Add the update site by clicking the button New Remote Site... and enter the followings:
          Name: jMoped Plug-in
          URL:  http://www7.in.tum.de/tools/jmoped/update/
      
    • Select the site you just added and click the Finish button. Follow the instructions and restart Eclipse afterwards.
  2. Native BDD library
    The plug-in is shipped together with JavaBDD—a pure Java implementation for manipulating BDDs. However, for a better performance, it is recommended to download one of the following pre-compiled CUDD libraries. It should work simply by putting one of the file in the Eclipse directory. If not, you will need to tell Eclipse where to find the library by appending the option -vmargs -Djava.library.path=/path/to/the/library when starting Eclipse.
  3. Annotations
    If you wish to use jMoped's annotations, you will need to include jmoped-translator.jar in Eclipse's Java build path.
  4. Examples

Source codes

jMoped is divided into four parts. All of them can be found on our SVN server.
  1. jwpds—a java library for weighted pushdown systems
    svn co "https://svn.model.in.tum.de/svn/jwpds/trunk" jwpds
    
  2. underbone—a model checker based on jwpds
    require: jwpds
    svn co "https://svn.model.in.tum.de/svn/underbone/trunk" underbone
    
  3. translator—translates Java bytecodes to Remopla models
    require: jwpds and underbone
    svn co "https://svn.model.in.tum.de/svn/jmoped-translator/trunk" jmoped-translator
    
  4. plug-in—the Eclipse plug-in
    require: jwpds, underbone, and the translator
    svn co "https://svn.model.in.tum.de/svn/jmoped/trunk" jmoped
    

Usage

After installing the plug-in, open the jMoped progress view by choosing Window -> Show View -> Other..., and then jMoped -> jMoped. Note that for the first time the progress view might be opened at the bottom part of Eclipse. It is recommended to move it to the left part of Eclipse (by drag-and-drop), where it is designed to be displayed. See the screenshots.
  • Open a Java program to be tested.
  • Choose the default bits of variables and the heap size in the progress view. The heap size can be at most 2^bits - 1.
  • To start the analysis, right-click on the method to be tested, and choose Run As -> jMoped.
  • jMoped will simulate the method with all possible parameter values within the given range. Markers will appear on the left of Java statements. Their meanings are:

    Not Covered Not covered
    Partially Covered Partially covered
    Covered Covered
    Assertion Violation Assertion Violation
    Not Enough Heap Not Enough Heap
    NullPointerException NullPointerException
    ArrayIndexOutOfBoundException ArrayIndexOutOfBoundException
For sequential programs only:
  • It is also possible to just "execute" all test cases one-by-one instead of simulating them simultaneously by checking Execute Remopla in the progress view.
  • When an assertion is violated, you can click on the red marker to generate all counterexamples that lead to the error. Then, by right-clicking these counterexamples, a JUnit test case will be created.
For multithreaded programs only:
  • Choose the thread bound and context bound from the progress view. The thread bound fixes the number of threads you can create. The context bound determines the number of times in which threads can get active. jMoped analyzes all possible thread interactions up to the bound.
  • The Lazy splitting option in the progress view tries to switch contexts lazily. jMoped usually runs faster when this option is on.

Command-line translator

jMoped internally translates Java bytecodes into a language for pushdown systems called Remopla—an input language of Moped. If you wish to use Moped from a command-line (i.e. without the Eclipse plug-in) for checking Java programs, you might consider downloading the following jar file to generate the Remopla models.

Download: translator.jar (Updated: 15.10.2008)

Usage:
java -jar translator.jar [package/]class.method bits heapsize [classpath1 ...]
will print out the Remopla model. You can then redirect it to a file (by using e.g. >).

Remarks:
  • jMoped's annotations only work when debugging info is included in the class files, i.e. the source files must be compiled with -g option.
  • method must include a method name and its descriptor. Method descriptors must be in the form specified by the java virtual machine specification. For instance, for the method void sort(int[] array) in class Quicksort of pakcage de/tum/in/sort, you will need to input "de.tum.in.sort/Quicksort.sort([I)V" as the first argument.
  • You will need to tell the translator where to find all relevant classes. There are two ways to do this: (i) Appends all paths in the command-line. (ii) Creates a file named classpath and put all paths in it. The syntax is the same as when you set the CLASSPATH variable for Java, i.e. using colon-separated paths (path1:path2:path3).

Documentations

See
  • poster and paper at CAV'07 to catch a glimpse of jMoped,
  • paper at SPIN'08 for the theory behind the support of multi-threaded programs including a brief on the translator,
  • FAQs page,
  • diploma thesis of Felix Berger.

Limitations

The current jMoped supports all common Java features, however some obvious limitations are:
  1. The parameters of the inital method can only have types: primitive integer (int), array of primitive integers (int[]), and Integer class (java.lang.Integer).
  2. Programs that use Java library might not work correctly, since they sometimes involve native codes.
  3. String support is very poor. Basically, jMoped supports String variables, but none of their operations (including concatenation).

Contact

jMoped 2.0 is written and maintained by Dejvuth Suwimonteerabuth. Some parts of the code were taken from jMoped 1.0 contributed also by Stefan Schwoon and Felix Berger.


Links

This page has been outdated since 25.02.2009.