Using the Bandera Tool Set and JPF to Model-check Properties of Concurrent Java Software

Presented by :

John Hatcliff and Matthew Dwyer, Department of Computer Science, Kansas State University

Willem Visser, RIACS, NASA Ames

April 13, 2002, full day

Abstract :

The Bandera Tool Set is an integrated collection of program analysis, transformation, and visualization components designed to facilitate experimentation with model-checking Java source code. Bandera takes as input Java source code and a software requirement formalized in Bandera's temporal specification language, and it generates a program model and specification in the input language of one of several existing model-checking tools (including Spin, dSpin, SMV) and and the JPF model-checker from NASA Ames. Both program slicing and user extensible abstract interpretation components are applied to customize the program model to the property being checked. When a model-checker produces an error trail, Bandera renders the error trail at the source code level and provides a number of facilities for visualizing the path of the trail through the source code while displaying values of variables and internal states of Java lock objects.

JPF is an explicit-state model-checker that works directly on Java bytecode. It has a very flexible architecture and includes a number of components that complement traditional model-checking including run-time monitoring facilities, heuristic search capabilities, components to provide coverage information.

In this tutorial, we will guide participants through the process of applying Bandera and JPF to model-check temporal properties of concurrent Java programs with examples drawn from well-known concurrency texts and standard Java libraries. This will include modules on using Bandera's temporal specification language, effectively applying Bandera's slicing, abstraction facilities, and counterexample display facilities, and JPF's heuristic search strategies. In addition, we will give an overview of case-studies that involved applying Bandera and JPF to check properties of several avionics and flight-control systems.

This tutorial will use an upgraded version of Bandera and the most recent version of JPF. Participants will receive CDs that hold these versions of Bandera and JPF, the Bandera tutorial, an examples repository that includes the examples used in the tutorial, and the PowerPoint slides from the tutorial.