GSoC/GCI Archive
GSoC/GCI Archive
Google Summer of Code 2011

The Java Pathfinder Team

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

Mailing List: http://groups.google.com/group/java-pathfinder

The Java PathFinder project (JPF) was initially conceived and developed at NASA Ames Research Center in 1999. JPF 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 2011 is led 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. As JPF has matured in its ability to perform verification on traditional Java programs, we in the process of extending JPF to verify software running on mobile devices. Given that Android is one of the largest open-source framework for mobile computing, we are extending JPF to specifically verify Android applications and the also the Android operating systems.

Projects

  • Backtrackable FileSystem In the current implementation of JPF all java.io.* peers operations with filesystem aren't backtrackable. This proposal describes an idea to implement file operations in backtrackable way, so that SUT that performs operation with file system could be correctly tested under JPF.
  • Checking Human Machine Interactions The goal of the project is to robustify the jpf-hmi extension that has been started last year. Such extension allows to check human-machine interaction, by analysing system and mental models, modelled with LTSs encoded as JPF-statecharts. The HMI analysis is based on a full-control property. The project aims at integrating the ADEPT toolset developed at NASA Ames.
  • Checking Java Annotations Imagine the world where computers are handling all critical situations. In order to maximize application reliability, production versions should not differ from the testing version. Achieving that is possible using annotations which are detected at runtime. The aim of Checking Java Annotation project is to develop a set of annotations that can be applied to Java programs to assist tools that detect software defects.
  • Detecting Infinite Loops Checking software termination is, in general, undecidable, but has been shown decidable for certain classes of programs. In particular, termination checking for loops with linear assignments is decidable. This project aims to create an extension for Java Pathfinder which can determine whether non-terminating loops of this form are present in a given program.
  • Effective representation of symbolic execution tree for SPF This project implements an efficient trie-based data structure representation for the symbolic execution tree for Symbolic Pathfinder. The goal is to define a data structure that compactly represents symbolic execution tree and can be maintained on-the-fly, as the program undergoes changes.
  • Generate JPF option lists from code The goal of this project is to develop tool collecting all JPF options and writing them in one popular data format – XML. The result of using this tool is list containing all potential options: key and type of each option (with annotation if available).
  • Improving Error Discovery of the Slicing and Dicing Technique The slicing and dicing verification technique attempts to reduce the state space that needs to be explored to find errors in concurrent programs. New threads are added to the concrete execution using an iterative refinement of the current under-approximation. However, it does not currently handle the case where refinement locations are reachable along more than one path from the start of the program. This project aims to enhance it to verify complex multi-threaded programs such as these.
  • jpf-bdd, A jpf project for handling Boolean variables with Binary Decision Diagrams This project aims at extending the model checker Java Path Finder to handle a special set of Boolean variables using Binary Decision Diagrams (BDDs). This enables efficient verification of Java programs with a set of Boolean variables that are guiding the control flow. In this project I will use software product-lines as a concrete example for such programs. Verification of a product-line with JPF and the BDD-extension will be significantly faster than with a standard JPF-installation.
  • JPF-InspectorII I propose to extend the JPF-Inspector tool with several new features, including: backward single stepping, ­batch execution from command-line, program state modification, ­introspection of the JPF internal state, simple integration with IDE, UI improvements, profiling info. The goal is to improve the JPF-Inspector and make it a mature and useful tool.
  • JPF-Regression: Extending DiSE for Inter-procedural Analysis Though DiSE provides an interesting new way of analyzing changes between program versions within individual methods, it is important to recognize that methods will often interact. By extending the tool from being just intra-procedural to also being inter-procedural, DiSE will be able to determine the effects that changes have across a broader scope of a program. This will make DiSE's hybrid approach to program verification much more powerful.
  • Support for new Java concurrency primitives & Extending support for Java 1.5 concurrency constructs java.util.concurrent contains many classes including native methods. The jpf-concurrent project supports many of these classes by using model classes and native peer classes. A part of java.util.concurrent is java.util.concurrent.atomic which can be used to implement lock-free algorithms. This project includes providing support for unhandled native calls within java.util.concurrent. Moreover, regression tests will be performed to ensure the compatibility of this package with jpf-concurrent.