Skip to main content
SpringerLink
Log in
Book cover

International SPIN Workshop on Model Checking of Software

SPIN 1999: Theoretical and Practical Aspects of SPIN Model Checking pp 216–231Cite as

Applying Model Checking in Java Verification

  • Conference paper
  • First Online:

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

Abstract

This paper presents our experiences in applying the Java PathFinder (Jpf), a recently developed Java to Promela translator, in the search for synchronization bugs in a Chinese Chess game server application written in Java. We give an overview of Jpf and the subset of Java that it supports and describe an initial effort to abstract and analyze the game server. Finally, we evaluate the results of the effort.

This is a preview of subscription content, 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. J. R. Burch, E. M. Clarke, K. L. McMillan, and D. L. Dill. Sequential circuit verification using symbolic model checking. In 27th ACM/IEEE Design Automation Conference, 1990.

    Google Scholar 

  2. R. Iosif C. Demartini and R. Sisto. Modeling and Validation of Java Multithreading Applications using SPIN. In G. Holzmann, E. Najm, and A. S erhrouchni, editors, Proceedings of the 4th SPIN workshop, Paris, France, November 1998.

    Google Scholar 

  3. T. Cattel. Modeling and Verification of sC++ Applications. In Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, Lisbon, Portugal, LNCS 1384, April 1998.

    Google Scholar 

  4. J. C. Corbett. Constructing Compact Models of Concurrent Java Programs. In Proceedings of the ACM Sigsoft Symposium on Software Testing and Analysis, Clearwater Beach, Florida., March 1998.

    Google Scholar 

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

    Google Scholar 

  6. W. de Roever, H. Langmaack, and A. Pnueli (Eds.). Compositionality: The Significant Difference, International Symposium, COMPOS’97, Bad Malente, Germany. LNCS 1536. Springer-Verlag, September 1997.

    Google Scholar 

  7. P. Godefroid. Model checking for programming languages using Verisoft. In ACM Symposium on Principles of Programming Languages, pages 174–186, Paris, January 1997.

    Google Scholar 

  8. J. Gosling, B. J oy, and G. Steele. The Java Language Specification. The Java Series. A-W, 1996.

    Google Scholar 

  9. S. Graf and H. Saidi. Construction of abstract state graphs with PVS. In O. Grumberg, editor, CAV. Springer-Verlag, June 1997.

    Google Scholar 

  10. J. Hatcli-, M. Dwyer, S. Laubach, and D. Schmidt. Stating static analysis using abstraction-based program specialization, 1998.

    Google Scholar 

  11. K. Havelund, M. Lowry, and J. Penix. Formal Analysis of a Space Craft Controller using SPIN. In G. Holzmann, E. Najm, and A. Serhrouchni, editors, Proceedings of the 4th SPIN workshop, Paris, France, November 1998.

    Google Scholar 

  12. K. Havelund and T. Pressburger. Model Checking Java Programs using Java PathFinder. NASA Ames Research Center. To appear in the International Journal on Software Tools for Technology Transfer (STTT), 1999.

    Google Scholar 

  13. Gerard Holzmann. The Design and Validation of Computer Protocols. Prentice Hall, 1991.

    Google Scholar 

  14. N. D. Jones, editor. Special Issue on Partial Evaluation, 1993 (Journal of Functional Programming, vol. 3, no. 4). Cambridge University Press, 1993.

    Google Scholar 

  15. K.L. McMillan. Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, 1993.

    Google Scholar 

  16. G. Naumovich, G.S. Avrunin, and L.A. Clarke. Data flow analysis for checking properties of concurrent java programs. Technical Report 98-22, Computer Science Department, University of Massachusetts at Amherst, April 1998.

    Google Scholar 

  17. B. Pell, E. Gat, R. Keesing, N. Muscettola, and B. S mith. Plan Execution for Autonomous Spacecrafts. In Proceedings of the 1997 International Joint Conference on Artificial Intelligence, 1997.

    Google Scholar 

  18. F. Tip. A survey of program slicing techniques. Journal of Programming Languages, 3(3):121–189, 1995.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. NASA Ames Research Center, Recom Technologies, Moffett Field, CA, USA

    Klaus Havelund

  2. Computer Systems Laboratory, Stanford University, Stanford, CA, 94305, USA

    Jens Ulrik Skakkebæk

Authors
  1. Klaus Havelund
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jens Ulrik Skakkebæk
    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

Havelund, K., Skakkebæk, J.U. (1999). Applying Model Checking in Java Verification. 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_17

Download citation

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

  • 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