A Generic ESC/Java2 Plugin and Verification Plugin Facade for Java IDEs
Supervisor Dermot Cochran
Subject Area Software Engineering
Pre-requisite Good knowledge of Java and at least one IDE
Co-requisite Knowledge of the Eclipse platform, component models,
formal software engineering processes, and
verification will be obtained during the course of
this project
Subject Coverage Integrated Development Environments, Formal
Specifications, Extended Static Checking,
Verification, Logic
Project Type Design & Implementation
Hardware PC or workstation (on nearly any operating system)
Description
JML is the de facto standard behavioral specification language for
Java. Many powerful research tools understand JML, including
ESC/Java2. ESC/Java2 is the world's most advanced extended static
checker. It is based upon the ESC/Java tool from Digital Systems
Research Lab. ESC/Java2 automatically checks that a Java program
conforms to its JML formal specification. ESC/Java2 works just like a
compiler via a command-line interface. A basic graphical Swing-based
interface exists as well.
A few groups have written research prototypes of basic ESC/Java2 and
ESC/Java plugins for the Eclipse platform. None of these plugins offer
any functionality beyond push-button execution and code highlighting
for syntax, type, and verification errors.
The goal of this project is to extend one of these existing plugins to
create a rich, full-featured plugin for ESC/Java2. Such a plugin would
include functionality for tracking verification goals, externally
motivated reasons for new annotations or changes to existing
annotations, integration with version control systems (particularly
with regards to commit policies), etc.
Additionally, in the long run we wish to support all major integrated
development environments, thus the plugin needs to be sufficiently
abstracted so as to work in several different component models. To
obtain this goal the component plugin models of several main IDEs will
be analyzed and their core functionality will represented via a
verification plugin facade. Thus, the student that works on this
project will gain a great deal of experience with all major Open
Source and commercial IDEs including Eclipse, NetBeans, IDEA,
VisualStudio, CodeGuide, jCreator, jBuilder, jStudio, etc., including
more "generic" IDEs like jEdit, SlickEdit, and Emacs.
Mandatory
1) Gain familiarity with JML and ESC/Java2.
2) Become familiar with several IDEs, primary among them Eclipse,
IDEA, NetBeans, VisualStudio, and jBuilder.
3) Analyze component plugin models of IDEs.
4) Design verification facade component model.
5) Implement verification facade component model.
6) Perform requirements analysis and design ESC/Java2 plugin.
7) Implement ESC/Java2 plugin.
8) Demonstrate working plugin in at least two IDEs.
9) Release plugin with new version of ESC/Java2. Release verification
facade plugin and component model also as a separate product. Fame and
fortune follow.
Discretionary
1) Demonstrate working plugin in all primary IDEs.
2) Implement facade model for all secondary IDEs.
3) Write, submit, and publish a paper on the results.
Exceptional
Analyzing the component model from a generic point of view and
proposing a component model theory that formalizes its features earns
an M.S. :)
Sources of information and preparatory reading
1) The JML web site http://www.jmlspecs.org/
2) The ESC/Java2 web site http://www.kindsoftware.com/products/opensource/ESCJava2/
3) Read the two recent papers available via the JML web page: "An
overview of JML tools and applications" and "JML: notations and tools
supporting detailed design in Java".
4) Read "ESC/Java2: Uniting ESC/Java and JML: Progress and issues in
building and using ESC/Java2" available via
http://www.kindsoftware.com/~kiniry/papers/NIII-R0413.pdf
5) Download, install, and play around with the JML tool suite and
ESC/Java2 to get a feel for the technology.
6) Download, install, and play around with
Eclipse. http://www.eclipse.org/
7) Find, download, install, and review existing ESC/Java and ESC/Java2
plugins.
