Skip to main content
SpringerLink
Log in

Assume-Guarantee Model Checking of Software: A Comparative Case Study

  • Conference paper
  • First Online:
Theoretical and Practical Aspects of SPIN Model Checking (SPIN 1999)

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

Included in the following conference series:

Abstract

A variety of assume-guarantee model checking approaches have been proposed in the literature. In this paper, we describe several possible implementations of those approaches for checking properties of software components (units) using SPIN and SMV model checkers. Model checking software units requires, in general, the definition of an environment which establishes the run-time context in which the unit executes. We describe how implementations of such environments can be synthesized from specifications of assumed environment behavior written in LTL. Those environments can then be used to check properties that the software unit must guarantee which can be written in LTL or ACTL. We report on several experiments that provide evidence about the relative performance of the different assume-guarantee approaches.

This work was supported in part by NSF and DARPA under grants CCR-9633388, CCR-9703094, and CCR-9708184 and by NASA under grant NAG-02-1209.

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

Access this chapter

Log in via an institution
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. M. Abadi and L. Lamport. Composing specifications. ACM Transactions on Programming Languages and Systems, 15(1):73–132, January 1993.

    Article  MATH  Google Scholar 

  2. J. Atlee and J. Gannon. State-based model checking of event-driven system requirements. IEEE Transactions on Software Engineering, 19(1):24–40, June 1993.

    Article  Google Scholar 

  3. G.S. Avrunin, J.C. Corbett, and L.K. Dillon. Analyzing partially-implemented real-time systems. In Proceedings of the 19th International Conference on Software Engineering, May 1997.

    Google Scholar 

  4. A.T. Chamillard. An Empirical Comparison of Static Concurrency Analysis Techniques. PhD thesis, University of Massachusetts at Amherst, May 1996.

    Google Scholar 

  5. S.C. Cheung and J. Kramer. Checking subsystem safety properties in compositional reachability analysis. In Proceedings of the 18th International Conference on Software Engineering, Berlin, March 1996.

    Google Scholar 

  6. E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, April 1986.

    Article  MATH  Google Scholar 

  7. J.C. Corbett. Evaluating deadlock detection methods for concurrent software.IEEE Transactions on Software Engineering, 22(3), March 1996.

    Google Scholar 

  8. 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 

  9. M.B. Dwyer and C.S. P-as-areanu. Filter-based model checking of partial systems. In Proceedings of the Sixth ACM SIGSOFT Symposium on Foundations of Software Engineering, November 1998.

    Google Scholar 

  10. M.B. Dwyer and C.S. P-as-areanu. Model checking generic container implementations. In Generic Programing: Proceedings of a Dagstuhl Seminar, Lecture Notes in Computer Science, Dagstuhl Castle, Germany, 1998. to appear. Assume-Guarantee Model Checking of Software: A Comparative Case Study 183

    Google Scholar 

  11. M.B. Dwyer, C.S. P-as-areanu, and J.C. Corbett. Translating ada programs for model checking: A tutorial. Technical Report 98-12, Kansas State University, Department of Computing and Information Sciences, 1998.

    Google Scholar 

  12. 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 

  13. R. Gerth, D. Peled, M.Y. Vardi, and P. Wolper. Simple On-the-fly Automatic Verification of Linear Temporal Logic. In Proceedings of PSTV’95, 1995.

    Google Scholar 

  14. O. Grumberg and D.E. Long. Model Checking and Modular Verification. ACM Transactions on Programming Languages and Systems, 16(3):843–871, May 1994.

    Article  Google Scholar 

  15. K. Havelund and T. Pressburger.Model checking java programs using java pathfinder. International Journal on Software Tools for Technology Transfer, 1999.to appear.

    Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  17. R. Iosef. A concurrency analysis tool for java programs. Master’s thesis, Polytechnic University of Turin, August 1997.

    Google Scholar 

  18. N.D. Jones, C.K. Gomard, and P. Sestoft. Partial Evaluation and Automatic Program Generation. Prentice-Hall International, 1993.

    Google Scholar 

  19. O. Kupferman and M.Y. Vardi. On the complexity of branching modular model checking (extended abstract). In Insup Lee and Scott A. Smolka, editors, CONCUR’ 95: Concurrency Theory, 6th International Conference, volume 962 of Lecture Notes in Computer Science, pages 408–422, Philadelphia, Pennsylvania, 21-24 August 1995. Springer-Verlag.

    Google Scholar 

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

    Google Scholar 

  21. Z. Manna and P. Wolper. Synthesis of communicating processes from temporal logic. ACM Transactions on Programming Languages and Systems (TOPLAS), 6(1):68–93, 1984.

    Article  Google Scholar 

  22. K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.

    Google Scholar 

  23. G.N. Naumovich, G.S. Avrunin, L.A. Clarke, and L.J. Osterweil. Applying static analysis to software architectures. In LNCS 1301. The 6th European Software Engineering Conference held jointly with the 5th ACM SIGSOFT Symposium on the Foundations of Software Engineering, September 1997.

    Google Scholar 

  24. C.S. P-as-areanu, M.B. Dwyer, and M. Huth. Modular Verification of Software Units. Technical Report 98-15, Kansas State University, Department of Computing and Information Sciences, 1998.

    Google Scholar 

  25. C.S. P-as-areanu and M.B. Dwyer. Software Model Checking Case Studies. http://www.cis.ksu.edu/santos/bandera/index.html#case-studies, 1998.

  26. A. Pnueli. In transition from global to modular temporal reasoning about programs. In K. Apt, editor, Logics and Models of Concurrent Systems, pages 123–144. Springer-Verlag, 1985.

    Google Scholar 

  27. M.Y. Vardi. On the complexity of modular model checking. In Proceedings, Tenth Annual IEEE Symposium on Logic in Computer Science, pages 101–111, San Diego, California, 26-29 June 1995. IEEE Computer Society Press.

    Google Scholar 

  28. P. Wolper. Specifying interesting properties of programs in propositional temporal logics. In Proceedings of the 13th ACM Symposium on Principles of Programming Languages, pages 184–193, St. Petersburg, Fla., January 1986.

    Google Scholar 

  29. M. Young, R.N. Taylor, D.L. Levine, K.A. Nies, and D. Brodbeck. A concurrency analysis tool suite: Rationale, design, and preliminary experience. ACM Transactions on Software Engineering and Methodology, 4(1):64–106, January 1995.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

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

    Corina S. Păsăreanu

Authors
  1. Corina S. Păsăreanu
    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. Michael Huth
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Electrical Engineering and Department of Mathematics and Computer Science, Eindhoven University of Technology, 5600, MB Eindhoven, The Netherlands

    Dennis Dams

  2. Intel Microprocessor Products Group, Strategic CAD Laboratories, 5200 NE Elam Young Parkway, JFT-104, Hillsboro, OR, 97124-6497, USA

    Rob Gerth

  3. Department of Electrical and Computer Engineering, University of Waterloo, Waterloo, Ontario, N2L 3G1, Canada

    Stefan Leue

  4. C.N.R.-Ist., CNUCE via Santa Maria 36, 56126, Pisa, Italy

    Mieke Massink

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Păsăreanu, C.S., Dwyer, M.B., Huth, M. (1999). Assume-Guarantee Model Checking of Software: A Comparative Case Study. In: Dams, D., Gerth, R., Leue, S., Massink, M. (eds) Theoretical and Practical Aspects of SPIN Model Checking. SPIN 1999. Lecture Notes in Computer Science, vol 1680. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48234-2_14

Download citation

  • DOI: https://doi.org/10.1007/3-540-48234-2_14

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66499-4

  • Online ISBN: 978-3-540-48234-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation