jMoped 2.0


	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

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

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://archive.model.in.tum.de/tools/jmoped/update/
```
- Select the site you just added and click the Finish button. Follow the instructions and restart Eclipse afterwards.
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.
- 32-bit Linux
- 64-bit Linux
- 32-bit Mac OS X
- 64-bit Mac OS X (many thanks to Christian Kern!)
- Windows
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.
Annotations
If you wish to use jMoped's annotations, you will need to include jmoped-translator.jar in Eclipse's Java build path.
Examples

Source codes

jMoped is divided into four parts. All of them can be found on our SVN server.

jwpds—a java library for weighted pushdown systems

svn co "https://svn.model.in.tum.de/svn/jwpds/trunk" jwpds

underbone—a model checker based on jwpds
require: jwpds

svn co "https://svn.model.in.tum.de/svn/underbone/trunk" underbone

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

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
	Partially covered
	Covered
	Assertion Violation
	Not Enough Heap
	NullPointerException
	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:

The parameters of the inital method can only have types: primitive integer (int), array of primitive integers (int[]), and Integer class (java.lang.Integer).
Programs that use Java library might not work correctly, since they sometimes involve native codes.
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.