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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
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.
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.
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.
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.
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.
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.
P. Godefroid. Model checking for programming languages using Verisoft. In ACM Symposium on Principles of Programming Languages, pages 174–186, Paris, January 1997.
J. Gosling, B. J oy, and G. Steele. The Java Language Specification. The Java Series. A-W, 1996.
S. Graf and H. Saidi. Construction of abstract state graphs with PVS. In O. Grumberg, editor, CAV. Springer-Verlag, June 1997.
J. Hatcli-, M. Dwyer, S. Laubach, and D. Schmidt. Stating static analysis using abstraction-based program specialization, 1998.
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.
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.
Gerard Holzmann. The Design and Validation of Computer Protocols. Prentice Hall, 1991.
N. D. Jones, editor. Special Issue on Partial Evaluation, 1993 (Journal of Functional Programming, vol. 3, no. 4). Cambridge University Press, 1993.
K.L. McMillan. Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, 1993.
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.
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.
F. Tip. A survey of program slicing techniques. Journal of Programming Languages, 3(3):121–189, 1995.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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