A BRICS Mini-Course
October 2-4, 2000
Lectures by
John Hatcliff, hatcliff@cis.ksu.edu
Kansas State University
Finite-state verification techniques, such as model checking, have shown promise as a cost-effective means for finding defects in hardware designs. To date, the application of these techniques to software has been hindered by several obstacles. Chief among these is the problem of constructing a finite-state model that approximates the executable behavior of the software system of interest.
In this series of lectures, we describe an integrated collection of program analysis and transformation components, called Bandera, that enables the automatic extraction of safe, compact finite-state models from program source code. Bandera is a model compiler in the sense that it takes Java source code as input and compiles it a program model expressed in the input language of one of several existing verification tools including SMV, Spin, and the JPF Java byte-code model-checker from NASA Ames. 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 allows the user to replay program execution both forwards and backwards along the path of the counterexample.
The lecture series will begin with an overview talk and an extended tool demonstration that illustrate the functionality Bandera's major components with some simple examples. Next, we give a summary of how Bandera's extensible temporal property specification language can be used to specify temporal properties in terms of Java source code features. As time permits, we will discuss theoretical foundations and implementation strategies of Bandera's slicing and abstraction components, as well as the back-end strategies used in generating inputs for Spin, SMV, and JPF. We conclude with a discussion of other forms of automated tool support that we are currently working on that we believe are necessary for model-checking properties of large code bases, and we relate some experiences that we've had using Bandera to check properties of space-craft control software and next-generation avionics systems with collaborators at NASA Ames and Honeywell.