JET - JPF Eclipse Tools


This project aims at providing support for JPF specific programming within the Eclipse IDE. It differs from the jpf-shell? project by focusing on editing related tasks for JPF specific files such as NativePeers, whereas jpf-shell is meant to support running JPF and displaying its various outputs outside of an IDE.

Programming tasks supported by JET include especially creation of JPF projects, editing of JPF properties files, and NativePeer creation and navigation.


student: Matt Kirn <mattkse "at"> (MK)
mentor: Peter Mehlitz <pcmehlitz "at"> <PM>
co-mentor: Darko Marinov <marinov "at"> (DM)


Details about ongoing work can be found on:

The main programming tasks targeted by JET are

(1) JPF Project Creation

This will provide a wizard dialog to create a JPF project with the required directory structure, configuration files (e.g. and build scripts (build.xml). The actual creation is performed by the existing gov.nasa.jpf.tool.CreateProject class, the wizard mostly provides the required arguments such as project name and location.

(2) JPF Configuration Editing

JET supports editing, project properties ( and application properties (*.jpf) according to the JPF configuration model.

(2a) JPF site properties

  • Properties are configurable via the Eclipse preferences manager
  • A default setup is provided upon fresh install of plug-in. Error messages are displayed if the default setup is invalid on the user's system
  • Automated editing support consists of creating jpf-core, project name and respective extensions entries for selected jpf-core and project directories

(2b) JPF project properties

  • Each project can configure via a new category in the project properties manager
  • When creating a new JPF project, there is an option to launch the properties manager to configure the properties
  • All properties that can be overridden are displayed in the properties manager
  • User can finish without modifying properties and accept a default configuration
  • Automated editing support consists of selecting project specific classpath, native_classpath and sourcepath directories, providing default values according the standard JPF project layout

(2c) JPF app properties

  • User can create app property files by selecting a context menu item on a target class (signified by its location in src/examples or src/tests), which subsequently opens a GUI dialog for user input
  • All properties that can be overridden are displayed in the GUI dialog
  • User can finish without overriding any properties to accept a default configuration
  • Automated editing support consists of adding target and target_args entries according to the selected target class, and by adding the standard "<project-name> = ${config_path}" preamble

(3) NativePeer Creation/Navigation

This will provide support to create NativePeer classes, and to navigate between the native peer, the (optional) respective model class, and a respective standard library version of the model class (if any). These functions will be accessible through a new "Peer View" that is a specialization of the standard Eclipse "Outline View", tying together the aforementioned NativePeer, model and library class according to the following drawing.

peer view drawing

Creating a NativePeer class involves selecting the target (model) class, and then selecting the methods within this class for which NativePeer method stubs should be created. Based on these selections, the Eclipse plugin has to provide the following functions:

  • creating NativePeer sources with correct names (JPF_<model-class-package>_<model-class-name>) within the src/peers directory
  • computing correctly mangled NativePeer method names that include signature (model class argument types) and return type, according to the scheme described in devel/mji MJI?
  • setting required method modifiers (public static)
  • creating proper argument lists (which always start with a (MJIEnv env, int objref,..) prefix)
  • proper mapping of model class reference arguments or return types into int ref types (JPF internally uses int to represent reference values)
  • creating method stub bodies (with proper return values)

This should be based on bytecode model classes since there might not be any model sources (e.g. for standard library classes). To avoid classpath setup problems, it seems best to use the BCEL library to parse the selected model class files (*.class). Using BCEL instead of Java reflection deviates from the approach taken with the GenPeer tool that was part of JPF v4, but does not require providing complete SUT classpaths that are otherwise just relevant when running JPF (i.e. are usually specified in *.jpf application property files).

Navigation functions should allow jumping between corresponding methods in the associated NativePeer, the model and the library class, to be displayed in different editors. Library classes should be displayed in read-only editors

Program & Timeline

This project is funded by a NASA Ames Internship. It follows the GSoC timeline (start 05/24, finish 08/16)


The sources for this project are available from a Mercurial repository on

Project Blog

(most recent on top)

2010-06-09 (PM) - updated project description according to discussions

2010-05-21 (PM) - added some project description

2010-05-07 (NR) - project page created

Last modified 8 years ago Last modified on 06/10/2010 07:43:15 AM

Attachments (1)

Download all attachments as: .zip