The Bandera Tool Set is an integrated collection of program analysis, transformation, and visualization components designed to allow experimentation with model-checking properties of Java source code. Bandera takes as input Java source code and a specification written 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, JPF). When a model-checker produces an error trail, Bandera renders the error trail at the source code level and allows the user to step through the code along the path of the trail while displaying values of variables and internal states of Java lock objects.
This document describes the basic functionality of Bandera as presented by Bandera's graphical user interface. Section 2 describes the overall architecture of the tool set and summarizes the rationale and functionality of each component. Section 3 provides a brief description of how to install Bandera. Section 4 describes basic aspects of the Bandera User Interface (BUI). Section 5 gives a guided tour of the BUI and tool components using several different examples. Section 6 gives a detailed discussion of the Bandera Specification Language (BSL). Section 11 summarizes the subset of Java that is currently handled by Java, and provides a list of known bugs and limitations.
We assume that the reader is familiar with the general concepts of compiling and model-checking and possesses a basic understanding of temporal logics such as LTL [13] or CTL [1]. The reader does not need to know how to use a particular model-checker tool such as Spin or SMV, although familiarity with such a tool will aid in understanding of Bandera's internal processing.
For a short description of Bandera and motivation of its architecture see [2]. For an overview of temporal logic and model-checking techniques, see [11].