Bandera: Tools for Automated Reasoning about Software System Behaviour
by Matthew Dwyer, John Hatcliff, and David Schmidt
The Bandera Project aims to develop techniques and tools for automated
reasoning about software system behavior, and to apply these tools
to construct high-confidence mission-critical software. Automated
reasoning is achieved by (1) mechanically creating high-level
models of software systems using abstract interpretation and partial
evaluation technologies, and then (2) employing model-checking
techniques to automatically verify that software specifications
are satisfied by the model. This project is a collaborative effort
between the Laboratory for Specification, Analysis and Transformation
of Software (SANTOS) at Kansas State University and researchers
at the Universities of Hawaii and Massachusetts. Work in SANTOS
is supported in part by grants from the US National Aeronautics
and Space Administration (NASA), the Defense Advanced Research
Projects Agency (DARPA) and the National Science Foundation (NSF).
Modern mission-critical software systems tend to be highly complex
and concurrent, and they often have stringent correctness requirements.
Pre-deployment reasoning about system behavior is crucial in application
areas such as avionics, industrial, health care, military command-and-control
where the cost of failure in the field is extremely high. Unfortunately,
the inherent size and complexity of such systems prohibit classical
validation techniques, such as testing, from providing high levels
of assurance of reliability and correctness. Subtle timing-related
defects in concurrent and embedded systems are very difficult
to reveal through testing. To do so would generally require software
testers to exercise all feasible execution paths and all possible
interactions between software components. In modern systems, this
is virtually impossible, and many deployed systems fail when real-world
use leads to an execution path that was not foreseen by the software
designers. Better verification techniques are sorely needed.
The Bandera tools allow software designers and quality assurance
personnel to state properties about software source code that
must hold along all execution paths. For example, in a priority-based
concurrent system developers might want to assure that: (1) when
two components of different priority levels attempt to access
a shared resource the higher-priority components gets access first;
(2) when a component attempts to access a resource it eventually
succeeds. Ideally, the tools should automatically explore all
execution paths and check to see if the given properties hold.
With some properties this can be done, but in most cases the size
of the system and the complexity of the specification makes this
infeasible. In these cases, the user guides the tools in the construction
of a smaller abstract model of the software system, and then the
tools can automatically check to see if a given specification
holds in the model. If the property holds in the model and if
the model safely approximates the software system’s behavior,
this guarantees that the property also holds in the original software
system. If the property does not hold, the tools will generate
a counter-example - a trace in the model system that violates
the given property. By appropriately interpreting the counterexample,
one can locate the source of the offending defect in the system
being modeled.
In the process outlined above, safe and effective model creation
is crucial for the approach to be successful. To make automatic
checking tractable, the model must discard information about the
program that is irrelevant to the property being verified. However,
it must retain enough structure to reason about relevant execution
paths. The Bandera tools use abstract interpretation, a rigorous
semantics-based methodology for constructing static analyses of
programs, to form safe abstractions of software, and partial evaluation
and slicing techniques to build compact models. The figure gives
the architecture of the tool suite for reasoning about Java programs.
Given software component source code S and a property to be verified
P, a slicing tool then cuts away portions of S that are irrelevant
for verifying P. The user then selects abstract interpretation
definitions to be used in abstracting the remaining program components.
These definitions can be drawn from a library of common abstractions
or they can be defined from scratch. Once the abstractions are
specified, abstraction-based partial evaluation (ABPE) creates
an abstracted and specialized version of the source program. The
transition system generator compiles the abstract program to one
of several existing model-checking tool input languages. If verification
fails, counter-examples produced by the model-checking tools are
rendered in terms of the original source program.
We have applied this methodology to several software systems written
in Ada. We have validated correctness properties of a programming
framework that supports parallelization of worklist algorithms;
this framework has been used to implement a variety of scientific
computing applications. We have also performed unit-level verification
of generic stack, queue, and priority-queue implementations and
demonstrated the ability of model checking to detect realistic
implementation defects in such systems. The lessons learned from
these experiences have provided important validation of and feedback
to our ongoing design and implementation of Java model construction
tools. We are working with the automated software engineering
group at the NASA Ames Research Center to incorporate these tools
into their avionics software workbench.
More information about this project is available at:
http://www.cis.ksu.edu/~santos
Please contact:
Matthew Dwyer, John Hatcliff, and David Schmidt - SANTOS Laboratory,
Department of Computing and Information Sciences, Kansas State
University
E-mail: {dwyer, hatcliff, schmidt}@cis.ksu.edu
