OverviewjMoped 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.
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.
ScreenshotsSee some screenshots of jMoped testing a quicksort implementation.
- Java 5.0 or later
- Eclipse 3.3 or later
- JUnit 4 or later
Download & Installation
- 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.
- 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.
If you wish to use jMoped's annotations, you will need to include jmoped-translator.jar in Eclipse's Java build path.
Source codesjMoped 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
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
UsageAfter 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
- 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.
- 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 translatorjMoped 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)
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. >).
- 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).
- 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.
LimitationsThe 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).
ContactjMoped 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.
- jMoped 1.0: the first version of jMoped
- Moped: a model checker for pushdown systems
- jclasslib: library for reading Java bytecodes.
- JavaBDD: library for manipulating BDDs
This page has been outdated since 25.02.2009.