Abstract
Model checking techniques have been an effective means for finding subtle defects in hardware designs and communication protocols. 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 long, and potentially abstract, 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 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 will present an overview of several case studies using Bandera that provide positive evidence of the effectiveness of model checking realistic properties of non-trivial concurrent software. These case studies also point out the need for additional functionality to enable scaling of software model checking to even larger and more complex systems. Finally, we conclude with a description of the latest public release of the Bandera toolset and our plans for future functionality.
Chapter PDF
Similar content being viewed by others
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 IFIP International Federation for Information Processing
About this paper
Cite this paper
Dwyer, M. (2002). Software Model Checking: The Bandera Approach. In: Jacobs, B., Rensink, A. (eds) Formal Methods for Open Object-Based Distributed Systems V. FMOODS 2002. IFIP — The International Federation for Information Processing, vol 81. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35496-5_1
Download citation
DOI: https://doi.org/10.1007/978-0-387-35496-5_1
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-5268-7
Online ISBN: 978-0-387-35496-5
eBook Packages: Springer Book Archive