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

The Java Pathfinder Team

Web Page: https://sites.google.com/site/jpfgsoc2013/

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 2013 is led by the NASA Ames Research Center, but includes mentors from NCSU, University of Texas, University of Utah, 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.

JPF has been used for a variety of application domains and research topics such as verification of multi-threaded applications, graphical user interfaces, networking, and distributed applications. In addition to its continued presence in academia, JPF has matured enough to support verification of production code and frameworks such as Android. JPF is constantly being extended with support for verification of new types of properties for new types of application domains.

Projects

  • Abstract Model Checking Abstract Pathfinder is an existing extension of Java Pathfinder (JPF) which allows for different abstractions of numeric types during model checking with JPF. In this project, we will build upon it by investigating possible approaches to the use of predicates as a supplementary type of abstraction to what already exist in the Abstract Pathfinder. Furthermore, we will implement the chosen approach as a part of the project. The solution will address various important features of Java - such as objects, classes, fields, arrays, local variables - and constraints over numeric types. The overall goal of this project is to enable proper use of predicate abstraction in JPF with a well-defined and complete extension that has its own predicate language.
  • An Eclipse Plug-in for Library Specifications Learning through Testing and Model Checking In this project we are going to develop an Eclipse Plug-in which automatically learns the behavior specifications of library classes by combining testing and symbolic execution within a practically reasonable time cost. The behavior specifications are the correct call sequences with preconditions for each method call to a function defined in the class. The plug-in enables library developer checking whether the implementation complies with his/her mental model and it also reduces a library user’s effort to understand the correct specification of the library by reading through the documentation or comments with the library.
  • Analysis of biological models in Symbolic PathFinder This project aims at modelling biological systems in a Statechart dialect of Java and applying model checking techniques to verify properties of interest such as stabilization or consistency with respect to a set of laboratory experimental observations. In particular, the project will focus on the C. elegans roundworm, which is a model organism extensively used in biological research because of its simplicity and tractability. The project will provide implementations for the particular composition operator and abstractions used in these models. The tool to be developed should be simple, intuitive and user-friendly in order to actually be useful for biological researchers.
  • Automated Model Generation for Library Code The JPF model checker relies on so-called model classes in order to combat the notorious state space explosion problem. The burden of writing model class is almost entirely on the developer. To help the developer in this error prone and tedious task, a tool, called model-generator, has already been developed. However this tool generates only empty stubs, forcing the developer to add the desired behaviour manually. The goal of this project is to provide a tool that can generate model classes with behaviour automatically.
  • Combining JDart and Randoop Achieving high code coverage in testing of real-world software is challenging. High code coverage is important because code coverage gives a measure of how thoroughly the software has been tested. This proposal addresses the challenge of reaching high code coverage by proposing a novel iterative algorithm for generating unit tests in JDart. The algorithm exploits both random and systematic software testing and software verification techniques. Preliminary results show the algorithm outperforms existing techniques.
  • Computing Observable Modified Condition/Decision Coverage A significant issue when auto-generating tests is the effectiveness of the resulting test suite at finding faults. Structural coverage metrics, such as branch coverage, are used to guide automated test generation, but previous experiments have shown that such suites, when generated using model checking often do not provide good fault finding. This GSoC project will create an extension to JPF that will implement and evaluate automated test generation using a new test metric Observable Modified Condition/Decision Coverage (OMC/DC), which is an extension of the MC/DC metric that is used in safety-critical domains. Auto generated OMC/DC tests have been shown to be more effective at finding faults than MC/DC tests in a recent ICSE 2013 paper ("Observable Modified Condition/Decision Coverage" by Michael Whalen, Gregory Gay, Dongjiang You, Mats P. E. Heimdahl and Matt Staats) that targets data-flow programs (e.g. Simulink models). In this project, the notion of OMC/DC will be applied to Java files.
  • Habanero Deadlock Detector To keep up with the high demand of computer processing speed, concurrency will be important to the computer programming industry. Habanero Java (HJ) is a simple library that allows concurrency. Combined with Java Pathfinder (JPF), a user program can be run. JPF will then report if their program data-races, deadlocks, there are assertion violations or not. However, since HJ runtime library is fairly linear, and the concurrency scheduling is operating system dependent, it only looks at a small limited number of possible outcomes and may not find any data-races or deadlocks even if they are possible. Our project will help solve this problem, and find several possible outcomes of a precompiled HJ program with JPF. If a deadlock is possible, JPF will be able to report where the deadlock occurred.
  • Human assisted Parameterized Unit tests for GUI Testing This project aims at generating tests for GUI application by taking advantage of human written specification in form of parameterized unit test (PUT).
  • Invariant Discovery This proposal describes my plan to design, implement, evaluate, document, and release a novel framework for invariant discovery using JPF. The basic objective is to create an invariant discovery tool as well as to apply it to real-world artifacts to synthesize invariants for these artifacts.
  • Java Platform Debugger Architecture for Java Pathfinder The back-end for Java Platform Debugger Architecture based on JPF. It will allow using JPF instead of a common JVM for the purpose of debugging Java applications in any modern Java IDE. The aim is to provide users with all the features they are used to while debugging Java applications. The key task is to implement the Java Debug Wire Protocol specification on top of JPF that will make JPF more complete as a Java Virtual Machine.
  • JPF as Concurrency Teaching Assistant This project will involve extending Impendulo, a teaching system which records snapshots of code and performs analysis on them, by adding JPF to the existing toolchain. This will enable us to drastically improve analysis of concurrent programs and thereby determine where inexperienced programmers typically struggle when writing concurrent programs. Furthermore we can use our results to determine how well JPF compares to the current Impendulo toolchain with regards to finding concurrency bugs.
  • Secure Information Flow by Symbolic PathFinder This project is a continuation from last year, which aims to quantify leakage of confidential information in Java programs. This project focuses on analysing programs with unbounded loops.
  • Verification of LTL properties of Java code My aim in this project is to build jpf-ltl, a tool to perform verification of LTL properties of Java code that builds on top of Java Pathfinder and implements the nested depth-first search required for the verification of full LTL
  • Verifying Probabilistic Programs Leverage the strengths of both the JPF and PRISM model checkers in order to allow formal analysis for Java programs involving randomization or probabilistic features. Explore ways for JPF to take advantage of the reliability and performance present in the PRISM model checker.
  • Visual JPF The goal of this project is to facilitate a more visual and high-level understanding of JPF's textual log output. We will provide a visualization of individual execution states, the history of execution, as well as the execution tree of choices made by JPF. A more detailed account of the project description can be found at below JIVE website: http://www.cse.buffalo.edu/jive/JPF.pdf