Using the Bandera Tool Set to Model-check
Properties of Concurrent Java Software
John Hatcliff, Kansas State University

Finite-state verification techniques, such as model checking, have been an effective means for finding subtle defects in hardware designs. The increased use of concurrent software in embedded applications and the widespread adoption of Java with its built-in concurrency constructs have led researchers to attempt to adapt model-checking techniques to software. To date, this effort has been hindered by several obstacles including construction of correct tractable models from programs with enormous state spaces, appropriate specification of checkable software requirements, and interpretation of very long counterexample traces.

In this talk, we describe Bandera -- an integrated collection of tools for model-checking concurrent Java software that attempts to overcome the obstacles described above. Bandera is a model compiler in the sense that it takes Java source code as input and compiles it to a program model expressed in the input language of one of several existing verification tools including SMV, Spin, dSpin, and JPF. Program slicing and abstract interpretation components are used during compilation to customize the program model with respect to the properties being checked. Bandera is like a debugger in the sense that it maps counterexamples produced by back-end model checkers back to the source code level, and it allows the user to replay program execution both forwards and backwards along the path of the counterexample.

We illustrate the functionality of Bandera's major components with a demo of the tool on several examples. This will include an overview of how Bandera's extensible temporal property specification language can be used to specify temporal properties in terms of Java source code features. We summarize results of using Bandera to verify properties of safety-critical software including avionics applications. We conclude with a discussion of other forms of automated tool support that we are currently working on that we believe will be necessary for model-checking properties of large code bases.

Bandera Project Web site