The Java Pathfinder Team

Web Page: http://babelfish.arc.nasa.gov/trac/jpf/wiki/events/soc2010

Mailing List: java-pathfinder@googlegroups.com

The Java™ PathFinder project (JPF) was started at NASA Ames Research Center in 1999 and was open sourced in April 2005 as one of the first ongoing NASA development projects ever. JPF is a highly extensible Java™ Virtual Machine (JVM) written in Java itself, and is used to create a variety of verification tools ranging from concurrency software model checkers to test case generators using symbolic execution. JPF is a research platform and a production tool at the same time. Although JPF has serious contributions from companies and government agencies, our main user community is academic - there are ongoing collaborations with more than 20 universities world-wide. The JPF team for GSoC'10 is lead by the NASA Ames Research Center, but includes mentors from UIUC, NCSU, University of Texas, Brigham Young University and the universities of Stellenbosch SA, Tokyo JP and Prague CZ.

JPF is designed to be extensible. There are well defined extension mechanisms, directory structures and build procedures, which keep the core relatively stable and provide suitable, well separated testbeds for new ideas and alternative implementations. As a consequence we host a number of such extension projects on our own, public JPF server, together with a Wiki that is the one-stop for learning about, obtaining and contributing to JPF.

Projects

• Checking Human Machine Interactions This project will experiment with the use of JPF for checking properties of systems involving humans, user interfaces and the machine being controlled. It will focus on expressiveness of relevant properties, as well as analysis capabilities.
• Checking Java Annotation Imagine the world where computer systems are handling all critical situations. It is required that those systems are tested by powerful verification tools. In order to maximize application reliability, production version should not differ from testing version. Achievement of that is possible using annotations which are detected on runtime. Aim of Checking Java Annotation project is to develop set of annotations that can be applied to Java programs to assist tools that detect software defects.
• Construction of Linear Temporal Property verification extension JPF can verify various temporal properties, yet it hasn’t supported of generic temporal property verification (LTL or CTL). Presently,LTL-translator extension has implemented; however, Buechis received are quite generic, so there haven’t been any extension to check them. Thus, user must implement a corresponding listener to each property they want to verify. Hence, I propose a JPF extension that furnishes generic support for LTL and provide simpler way of concrete temporal property verification.
• Coverage Visualization This project involves developing new techniques for visualizing the residual coverage, the source-code portions that are not yet covered, in JPF. Visualization helps JPF users by assisting users in navigating both code under test and test code, thereby assisting users to understand and infer reasons of why certain code portions are not covered. This project will be implemented as an Eclipse plug-in by using Eclipse Visualization Toolkit including SWT, GEF, and Zest.
• Customizable Trace Server The trace server contains a database and two front ends, one for storing and one for querying data. During the execution of the SUT by JPF, a trace emitter captures events from JPF listener, add them some property values, and stores then using the trace storer interface. On the analysis side, a trace analyzer queries the database by using the trace query interface, generating a number of reports as a result. Report generation will allow events generated by extensions to be included in the trace.
• Extending String analysis in Symbolic Java Pathfinder Extend the symbolic execution to allow efficient string analysis of all Java string operations. The implementation should support both automata-based decision procedures for strings as well as bit-vector based approaches. For the former the Java String Analyzer (JSA) system can be used and for the latter HAMPI. The project should include a detailed comparison of these two approaches.
• LTL verification in JPF I propose an extension of Java Pathfinder (JPF) to verify a system under test (SUT) against linear temporal logic (LTL) formulae. This work will implement the double DFS algorithm to search the state space of the SUT, computed by JPF, and the Büchi automaton provided by the existing LTL2Buchi code, for violations of an LTL specification. Additionally, this work will provide the means to annotate Java code with LTL formulae in the style of the existing work in the jpf-aprop project.
• The JPF Inspector How many times during debugging do you want to make a step back and examine changes again? Error trace analysis is an evil, isn't it? What about a nice GUI, where you can single-step error trace and observe program state and variables? Does your environment test all possible branches? Are you interested in the code coverage of tested system? My Inspector tool will solve your problems.