Bild mit Unilogo
homeicon university sucheicon search siteicon sitemap kontakticon contact impressicon legal notice
unilogo University of Stuttgart 
SZS | Contact | People | Teaching | Research | Publications | Tools | Institute | Department | Links
Institute of Formal Methods in Computer Science

jMoped - A Translator from Java Bytecodes to Pushdown Systems
 

News

There is now an Eclipse plug-in for jMoped, see the new jMoped page.

To keep jMoped compatible with Moped version 2, we are now offering jMoped version 2, which translates Java bytecode into Remopla instead of pushdown rules.

Overview

Java compilers produce so-called bytecode, a kind of machine language interpreted by the Java Virtual Machine. jMoped can translate this bytecode into pushdown systems, which are the input of Moped. Moped can then be used to check reachability and LTL properties of the translated system. Although, some details have been changed since the introduction of the Remopla language, the idea of the translation process is explained in great detail in Remy's Master thesis and TACAS'05 paper.

Downloads

Requirements

jMoped requires Java 5.0 or later. Eclipse is recommended to compile the source.

Set-up procedures

Since version 2.2.3, jMoped should run without initial set-ups.

Usages

jmoped [-<options>] <file>

<file> can be either Java file or class file. Running jMoped without an option will produce a Remopla file having same name as file but with .rem extension.

Running just jmoped will display available options. Options that effect the output of jMoped are:

-n adds some instructions into the Remopla output, which will make the label NPE reachable if a NullPointerException occurs.
-o<outfile>  sets the output file to <outfile>
-s symplifies labels of the Remopla output. This option only works when no two methods have the same name.
-t uses another translation technique for heap manipulation. There is still no documentation at the moment. However, this option is supposed to work better with large programs.

There are also some options in the case where Moped is called directly from jMoped. Theses options are basically passed to Moped without effecting the translation results. Make sure that the path to Moped executable in jmoped.conf is set correctly.
-a runs Moped for checking reachability of the label, which indicates an assertion violation.
-e runs Moped for checking reachability of the label, which indicates a NullPointerException.
-h runs Moped for checking reachability of the label, which indicates a heap overflow.
-r<label>  runs Moped for checking reachability of <label>

There are example files in ex/ subdirectory. It contains some examples that should give some ideas how to use jMoped. For example, jmoped -a ex/QuickSort.java will check for assertion error of an quicksort implementation.

Configurations

This version of jMoped includes a file named jmoped.conf, which is the configuration file that tells how the translated file is going to look like. The most important parameters are "bit" and "heap size". "bit" tells how many bits integers inside the program will have (default=4). "heap size" tells the size of the heap which will directly effect the number of objects can be instantiated in a Java program (default=15).

Limitations

The current jMoped supports common Java features, however some obvious limitations are:
  1. Negative integer is not supported.
  2. Multi-threading is not supported.
  3. Very limited support of String.
  4. Programs that use Java library might not work correctly, since they sometimes involve native library.

Changes

  • 17.11.06: Version 2.2.3, classpath look-up procedure changed.
  • 07.11.06: Version 2.2.2, bug fix in command-line option --bits=<n>.
  • 11.10.06: Version 2.2.1, first public release of jMoped version 2.

jMoped version 1

This is the old version of jMoped, created for Moped version 1.

Downloads

Changes

  • 15.10.2004: Version 1.0.0, initial release of the tool
  • 20.10.2004: Eliminated the requirement to have Spin installed
  • 11.04.2005: Version 1.0.1, use Java-supported assert() instead of special error() method. Counterexamples are translated back to Java statements.
  • 13.04.2005: Bug fixed, incorrect path while including class files
  • 15.04.2005: Another example (BinaryHeap.java) added

Contact

jMoped is written and maintained by Dejvuth Suwimonteerabuth.

Links

  
last change 09.02.2007 (mailto ds) |  © University of Stuttgart | legal notice