Bandera: extracting finite-state models from Java source code

ABSTRACT

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. Current best-practice involves hand-construction of models which is expensive (prohibitive for all but the smallest systems), prone to errors (which can result in misleading verification results), and difficult to optimize (which is necessary to combat the exponential complexity of verification algorithms).In this paper, 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 takes as input Java source code and generates a program model in the input language of one of several existing verification tools; Bandera also maps verifier outputs back to the original source code. We discuss the major components of Bandera and give an overview of how it can be used to model check correctness properties of Java programs.

REFERENCES

• 1: James C. Corbett, Evaluating Deadlock Detection Methods for Concurrent Software, IEEE Transactions on Software Engineering, v.22 n.3, p.161-180, March 1996 [doi>10.1109/32.489078]
• 2: James C. Corbett, Constructing compact models of concurrent Java programs, Proceedings of the 1998 ACM SIGSOFT international symposium on Software testing and analysis, p.1-10, March 02-04, 1998, Clearwater Beach, Florida, United States
• 3: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 4: Claudio DeMartini , Radu Iosif , Riccardo Sisto, A deadlock detection tool for concurrent Java programs, Software—Practice & Experience, v.29 n.7, p.577-603, June 1999 [doi>10.1002/(SICI)1097-024X(199906)29:7<577::AID-SPE246>3.0.CO;2-V]
• 5: David L. Dill , Andreas J. Drexler , Alan J. Hu , C. Han Yang, Protocol Verification as a Hardware Design Aid, Proceedings of the 1991 IEEE International Conference on Computer Design on VLSI in Computer & Processors, p.522-525, October 11-14, 1992
• 6: Yifei Dong , C. R. Ramakrishnan, An Optimizing Compiler for Efficient Model Checking, Proceedings of the IFIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XII) and Protocol Specification, Testing and Verification (PSTV XIX), p.241-256, October 05-08, 1999
• 7: Matthew B. Dwyer , George S. Avrunin , James C. Corbett, Patterns in property specifications for finite-state verification, Proceedings of the 21st international conference on Software engineering, p.411-420, May 16-22, 1999, Los Angeles, California, United States [doi>10.1145/302405.302672]
• 8: John Hatcliff , James C. Corbett , Matthew B. Dwyer , Stefan Sokolowski , Hongjun Zheng, A Formal Study of Slicing for Multi-threaded Programs with JVM Concurrency Primitives, Proceedings of the 6th International Symposium on Static Analysis, p.1-18, September 22-24, 1999
• 9: John Hatcliff , Matthew B. Dwyer , Shawn Laubach, Staging Static Analyses Using Abstraction-Based Program Specialization, Proceedings of the 10th International Symposium on Principles of Declarative Programming, p.134-151, September 16-18, 1998
• 10: J. Hatcli, M. B. Dwyer, S. Laubach, and N. Muhammad. Specializing congurable systems for nite-state veri cation.Technical Report 98-4, Kansas State University, Department of Computing and Information Sciences, 1998.
• 11: John Hatcliff , Matthew B. Dwyer , Hongjun Zheng, Slicing Software for Model Construction, Higher-Order and Symbolic Computation, v.13 n.4, p.315-353, Dec. 1, 2000 [doi>10.1023/A:1026599015809]
• 12: K. Havelund, M. Lowry, and J. Penix. Formal analysis of a space craft controller using SPIN. In Proceedings of the 4th International SPIN Workshop, Nov. 1997.
• 13: K. Havelund and T. Pressburger. Model checking Java programs using Java PathFinder. International Journal on Software Tools for T echnolo gy T ransfer , 1999. to appear.
• 14: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 15: Gerard J. Holzmann, The Engineering of a Model Checker: The Gnu i-Protocol Case Study Revisited, Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking, p.232-244, September 21-24, 1999
• 16: Gerard J. Holzmann , Margaret H. Smith, Software Model Checking, Proceedings of the IFIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XII) and Protocol Specification, Testing and Verification (PSTV XIX), p.481-497, October 05-08, 1999
• 17: Susan Horwitz , Thomas Reps , David Binkley, Interprocedural slicing using dependence graphs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.12 n.1, p.26-60, Jan. 1990 [doi>10.1145/77606.77608]
• 18: Frank Huch, Verification of Erlang programs using abstract interpretation and model checking, Proceedings of the fourth ACM SIGPLAN international conference on Functional programming, p.261-272, September 27-29, 1999, Paris, France
• 19: Daniel Jackson , Craig A. Damon, Elements of Style: Analyzing a Software Design Feature with a Counterexample Detector, IEEE Transactions on Software Engineering, v.22 n.7, p.484-495, July 1996 [doi>10.1109/32.538605]
• 20: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• 21: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 22: Sam Owre , John M. Rushby , Natarajan Shankar, PVS: A Prototype Verification System, Proceedings of the 11th International Conference on Automated Deduction: Automated Deduction, p.748-752, June 15-18, 1992
• 23: R. V alle-Rai, L. Hendren, V. Sundaresan, P. Lam, E. Gagnon, and P. Co. Soot - a Ja va optimization framew ork. InProceedings of CASCON'99, Nov. 1999.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: Java

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation
          Subjects: Automata (e.g., finite, push-down, resource-bounded)

General Terms:
Design, Languages, Measurement, Performance, Theory, Verification

Keywords:
abstract interpretation, model checking, model extraction, program specialization, program verification, slicing