Title Integration of JavaPathfinder into Eclipse
Student Sandro Badame
Mentor Peter C. Mehlitz
Abstract
The goal of this project will be to bring a GUI (Graphical User Interface) to the Java Pathfinder (JPF) system through a plugin for Eclipse. JPF is a system that allows for Java bytecode to be explored for possible execution defects. The goal of this project is to facilitate the adoption of JPF as step in development by seamlessly integrating it into the Eclipse IDE. By creating a plugin in Eclipse for JPF, developers can easily have JPF run through their programs and search for possible errors in development. This plugin will serve as an easy to use GUI that will greatly simplify the process of using JPF by hiding the need to create property files and command line arguments.
 Development of this project will be divided into three parts, development a new JPF launch type, a new JPF perspective and creation of an update site for the plugin.
 The JPF launch type will allow for any java application being developed in Eclipse to be tested with JPF with the click of a button. The JPF launch type will include the ability to configure all JPF runtime settings alongside the standard configurations for Java applications. Most development for this part of the project will be done with the Eclipse API since there currently does not seem to be any changes needed in JPF to successfully create this launch type.
 The JPF perspective will give developers an intuitive way of understanding the output from JPF. After executing a test with JPF developers will be given the option to switch to the JPF perspective to view the results. The JPF perspective will consist of a view to see the JPF output, a view for the source code and two new views that will be developed specifically for JPF. A trace view will be developed that will give a graphical representation of the execution path and transitions that lead to an exception. Selecting a transition from the trace view will affect the transition view. The transition view will give information about the code executed; the value of the choice generator that led to the transition and the choice ends it.
  The final task will be to develop an eclipse update site fort he plugin. The update site will host the plugin and a JPF build. Having the update site will also the plugin to be completely instable within eclipse itself streamlining the entire installation process.