Skip to main content
SpringerLink
Log in

Foundations of the Bandera Abstraction Tools

  • Chapter
  • First Online:
The Essence of Computation

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2566))

Abstract

Current research is demonstrating that model-checking and other forms of automated finite-state verification can be effective for checking properties of software systems. Due to the exponential costs associated with model-checking, multiple forms of abstraction are often necessary to obtain system models that are tractable for automated checking.

The Bandera Tool Set provides multiple forms of automated support for compiling concurrent Java software systems to models that can be supplied to several different model-checking tools. In this paper, we describe the foundations of Bandera’s data abstraction mechanism which is used to reduce the cardinality (and the program’s state-space) of data domains in software to be model-checked. From a technical standpoint, the form of data abstraction used in Bandera is simple, and it is based on classical presentations of abstract interpretation. We describe the mechanisms that Bandera provides for declaring abstractions, for attaching abstractions to programs, and for generating abstracted programs and properties. The contributions of this work are the design and implementation of various forms of tool support required for effective application of data abstraction to software components written in a programming language like Java which has a rich set of linguistic features.

This work was supported in part by NSF under grants CCR-9703094, CCR-9708184, CCR-9896354, and CCR-9901605, by the U.S. Army Research Laboratory and the U.S. Army Research Office under agreement DAAD190110564, by DARPA/IXO’s PCES program through AFRL Contract F33615-00-C-3044, by NASA under grant NAG-02-1209, by Intel Corporation under grant 11462, and was performed for the Formal Verification of Integrated Modular Avionics Software Cooperative Agreement, NCC-1-399, sponsored by Honeywell Technology Center and NASA Langley Research Center.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. T. Ball and S. Rajamani. Bebop: a symbolic model-checker for boolean programs. In K. Havelund, editor, Proceedings of Seventh International SPIN Workshop, volume 1885 of Lecture Notes in Computer Science, pages 113–130. Springer-Verlag, 2000.

    Google Scholar 

  2. Saddek Bensalem, Yassine Lakhnech, and Sam Owre. Computing abstractions of infinite state systems compositionally and automatically. In Proc. 10th International Conference on Computer Aided Verification, June 1998.

    Google Scholar 

  3. G. Brat, K. Havelund, S. Park, and W. Visser. Java PathFinder — a second generation of a Java model-checker. In Proceedings of the Workshop on Advances in Verification, July 2000.

    Google Scholar 

  4. James C. Corbett, Matthew B. Dwyer, John Hatcliff, Shawn Laubach, Corina S. Păsăreanu, Robby, and Hongjun Zheng. Bandera: Extracting finite-state models from Java source code. In Proceedings of the 22nd International Conference on Software Engineering, June 2000.

    Google Scholar 

  5. James C. Corbett, Matthew B. Dwyer, John Hatcliff, and Robby. Expressing checkable properties of dynamic systems: The Bandera Specification Language. International Journal on Software Tools for Technology Transfer, 2002. To appear.

    Google Scholar 

  6. P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth Annual ACM Symposium on Principles of Programming Languages, pages 238–252, 1977.

    Google Scholar 

  7. G.J. Holzmann D. Dams, W. Hesse. Abstracting C with abC. In Proc. 14th International Conference on Computer Aided Verification, July 2002.

    Google Scholar 

  8. Dennis Dams, Rob Gerth, and Orna Grumberg. Abstract interpretation of reactive systems. ACM Transactions on Programming Languages and Systems, 19(2):253–291, March 1997.

    Article  Google Scholar 

  9. C. Demartini, R. Iosif, and R. Sisto. dSPIN: A dynamic extension of SPIN. In Theoretical and Applied Aspects of SPIN Model Checking (LNCS 1680), September 1999.

    Chapter  Google Scholar 

  10. Matthew B. Dwyer, John Hatcliff, Roby Joehanes, Shawn Laubach, Corina S. Păsăreanu, Robby, Willem Visser, and Hongjun Zheng. Tool-supported program abstraction for finite-state verification. In Proceedings of the 23rd International Conference on Software Engineering, May 2001.

    Google Scholar 

  11. M.B. Dwyer, G.S. Avrunin, and J.C. Corbett. Patterns in property specifications for finite-state verification. In Proceedings of the 21st International Conference on Software Engineering, May 1999.

    Google Scholar 

  12. M. M. Gallardo, J. Martínez, P. Merino, and E. Pimentel. SPIN: Extending SPIN with abstraction. In Proceedings of Ninth International SPIN Workshop, volume 2318 of Lecture Notes in Computer Science, pages 254–258. Springer-Verlag, 2002.

    Google Scholar 

  13. Carsten K. Gomard and Neil D. Jones. atCompiler generation by partial evaluation. In G. X. Ritter, editor, Information Processing’ 89. Proceedings of the IFIP 11th World Computer Congress, pages 1139–1144. IFIP, North-Holland, 1989.

    Google Scholar 

  14. John Hatcliff. An introduction to partial evaluation using a simple flowchart language. In John Hatcliff, Peter Thiemann, and Torben Mogensen, editors, Proceedings of the 1998 DIKU International Summer School on Partial Evaluation, Tutorials in Computer Science, Copenhagen, Denmark, June 1998.

    Google Scholar 

  15. G. Holzmann. Logic verification of ANSI-C code with SPIN. In K. Havelund, editor, Proceedings of Seventh International SPIN Workshop, volume 1885 of Lecture Notes in Computer Science, pages 131–147. Springer-Verlag, 2000.

    Google Scholar 

  16. Gerard J. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279–294, May 1997.

    Article  MathSciNet  Google Scholar 

  17. M. Huth and M. Ryan. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, 1999.

    Google Scholar 

  18. Radu Iosif, Matthew B. Dwyer, and John Hatcliff. Translating Java for multiple model checkers: the bandera back end. Technical Report 2002-1, SAnToS Laboratory Technical Report Series, Kansas State University, Department of Computing and Information Sciences, 2002.

    Google Scholar 

  19. Neil D. Jones, Carsten K. Gomard, and Peter Sestoft. Partial Evaluation and Automatic Program Generation. Prentice-Hall International, 1993.

    Google Scholar 

  20. Y. Kesten and A. Pnueli. Modularization and abstraction: The keys to formal verification. In L. Brim, J. Gruska, and J. Zlatuska, editors, The 23rd International Symposium on Mathematical Foundations of Computer Science, volume 1450 of Lecture Notes in Computer Science. Springer-Verlag, 1998.

    Google Scholar 

  21. T. Lev-Ami and M. Sagiv. TVLA: A framework for Kleene-based static analysis. In Proceedings of the 7th International Static Analysis Symposium (SAS’00), 2000.

    Google Scholar 

  22. Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1991.

    Google Scholar 

  23. Flemming Nielson, Hanne Riis Nielson, and Chris Hankin. Principles of Program Analysis. Springer Verlag, 1999.

    Google Scholar 

  24. S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In Proceedings of the 1th International Conference on Automated Deduction (LNCS 607), 1992.

    Google Scholar 

  25. Corina S. Păsăreanu. Abstraction and Modular Reasoning for the Verification of Software. PhD thesis, Kansas State University, 2001.

    Google Scholar 

  26. Corina S. Păsăreanu, Matthew B. Dwyer, and Michael Huth. Assume-guarantee model checking of software: A comparative case study. In Theoretical and Applied Aspects of SPIN Model Checking (LNCS 16 80), September 1999.

    Google Scholar 

  27. Corina S. Păsăreanu, Matthew B. Dwyer, and Willem Visser. Finding feasible counter-examples when model checking abstracted Java programs. In Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 2031 of Lecture Notes in Computer Science, April 2001.

    Google Scholar 

  28. Rupak Majumdar Thomas A. Henzinger, Ranjit Jhala and Gregoire Sutre. Lazy abstraction. In Proceedings of the 29th ACM Symposium on Principles of Programming Languages (POPL’02), 2002.

    Google Scholar 

  29. Raja Valle-Rai, Laurie Hendren, Vijay Sundaresan, Patrick Lam, Etienne Gagnon, and Phong Co. Soot-a Java optimization framework. In Proceedings of CASCON’99, November 1999.

    Google Scholar 

  30. Eran Yahav. Verifying safety properties of concurrent Java programs using 3-valued logic. In Proceedings of the 28th ACM Symposium on Principles of Programming Languages (POPL’01), pages 27–40, January 2001.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computing and Information Sciences, Kansas State University, 234 Nichols Hall, 66506, Manhattan, KS, USA

    John Hatcliff, Matthew B. Dwyer &  Robby

  2. Kestrel Technology, NASA Ames Research Center, 94035-1000, Moffet Field, CA, USA

    Corina S. Păsăreanu

Authors
  1. John Hatcliff
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Matthew B. Dwyer
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Corina S. Păsăreanu
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Robby
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. DIKU, University of Copenhagen, Universitetsparken 1, 2100, Copenhagen, Denmark

    Torben Æ. Mogensen

  2. Department of Computing and Information Sciences, Kansas State University, 234 Nichols Hall, 66506, Manhattan, KS, USA

    David A. Schmidt

  3. Department of Computer Science, University of Texas at Dallas, P.O. Box 830688, 75083, Richardson, TX, USA

    I. Hal Sudborough

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Hatcliff, J., Dwyer, M.B., Păsăreanu, C.S., Robby (2002). Foundations of the Bandera Abstraction Tools. In: Mogensen, T.Æ., Schmidt, D.A., Sudborough, I.H. (eds) The Essence of Computation. Lecture Notes in Computer Science, vol 2566. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36377-7_9

Download citation

  • DOI: https://doi.org/10.1007/3-540-36377-7_9

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-00326-7

  • Online ISBN: 978-3-540-36377-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation