Skip to main content
Springer Nature Link
Log in

Extending JML for Modular Specification and Verification of Multi-threaded Programs

  • Conference paper
ECOOP 2005 - Object-Oriented Programming (ECOOP 2005)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 3586))

Included in the following conference series:

  • 1099 Accesses

Abstract

The Java Modeling Language (JML) is a formal specification language for Java that allows developers to specify rich software contracts for interfaces and classes, using pre- and postconditions and invariants. Although JML has been widely studied and has robust tool support based on a variety of automated verification technologies, it shares a problem with many similar object-oriented specification languages—it currently only deals with sequential programs. In this paper, we extend JML to allow for effective specification of multi-threaded Java programs. The new constructs rely on the non-interference notion of method atomicity, and allow developers to specify locking and other non-interference properties of methods. Atomicity enables effective specification of method pre- and postconditions and supports Hoare-style modular reasoning about methods. Thus the new constructs mesh well with JML’s existing features. We validate the specification language design by specifying the behavior of a number of complex Java classes designed for use in multi-threaded programs. We also demonstrate that it is amenable to automated verification using model checking technology.

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

Access this chapter

Log in via an institution

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. Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer, STTT (2004) (to appear)

    Google Scholar 

  2. Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. Technical Report 98-06y, Iowa State University, Department of Computer Science (2004), See, http://www.jmlspecs.org

  3. Leavens, G.T., Cheon, Y., Clifton, C., Ruby, C., Cok, D.R.: How the design of JML accommodates both runtime assertion checking and formal verification. Science of Computer Programming 55, 185–208 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  4. Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D.R., Kiniry, J.: Jml reference manual. Department of Computer Science, Iowa State University (2005), Available from http://www.jmlspecs.org

  5. Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: Proceedings of the International Workshop on Construction and Analysis of Safe, Secure and Interoperable Smart Devices (2004) (to appear)

    Google Scholar 

  6. Meyer, B.: Object-oriented Software Construction. Prentice-Hall, Englewood Cliffs (1997)

    MATH  Google Scholar 

  7. SAnToS: SpEx Website (2003), http://spex.projects.cis.ksu.edu

  8. Robby, Rodríguez, E., Dwyer, M., Hatcliff, J.: Checking strong specifications using an extensible software model checking framework. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 404–420. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  9. Hatcliff, J., Robby, M., Dwyer, M.: Verifying atomicity specifications for concurrent object oriented software using model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 175–190. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  10. Pugh, W.: Fixing the java memory model. In: Proceedings of the ACM 1999 Conference on Java Grande, New York, USA, pp. 89–98. ACM Press, New York (1999)

    Chapter  Google Scholar 

  11. Flanagan, C., Freund, S.N.: Type-based race detection for java. In: Proceedings of the ACM SIGPLAN 2000 Conference on Programming Language Design and Implementation, New York, USA, pp. 219–232. ACM Press, New York (2000)

    Chapter  Google Scholar 

  12. Lea, D.: Concurrent Programming in Java, 2nd edn. Addison-Wesley, Reading (2000)

    Google Scholar 

  13. Raghavan, A.D., Leavens, G.T.: Desugaring JML method specifications. Technical Report 00-03d, Iowa State University, Department of Computer Science (2003)

    Google Scholar 

  14. Lerner, R.A.: Specifying Objects of Concurrent Systems. PhD thesis, School of Computer Science, Carnegie Mellon University, TR CMU–CS–91–131 (1991)

    Google Scholar 

  15. Boyland, J., Noble, J., Retert, W.: Capabilities for sharing. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol. 2072, pp. 1–27. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  16. Noble, J., Vitek, J., Potter, J.: Flexible alias protection. In: Jul, E. (ed.) ECOOP 1998. LNCS, vol. 1445, pp. 158–185. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  17. Müller, P., Poetzsch-Heffter, A.: Universes: A type system for alias and dependency control. Technical Report 279, Fernuniversität Hagen, Available from (2001), http://www.informatik.fernuni-hagen.de/pi5/publications.html+

  18. Borgida, A., Mylopoulos, J., Reiter, R.: On the frame problem in procedure specifications. IEEE Transactions on Software Engineering 21, 785–798 (1995)

    Article  Google Scholar 

  19. Lipton, R.J.: Reduction: a method of proving properties of parallel programs. Communications of the ACM 18, 717–721 (1975)

    Article  MATH  MathSciNet  Google Scholar 

  20. Flanagan, C., Qadeer, S.: Types for atomicity. In: Proceedings of the 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, pp. 1–12. ACM Press, New York (2003)

    Chapter  Google Scholar 

  21. Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)

    Google Scholar 

  22. Dwyer, M.B., Hatcliff, J., Robby, R., Prasad, V.: Exploiting object escape and locking information in partial order reduction for concurrent object-oriented programs. Formal Methods in System Design 25, 199–240 (2004)

    Article  MATH  Google Scholar 

  23. Dietl, W., Müller, P.: Universes: Lightweight ownership for jml. In: Journal of Object Technology (2005) (to appear)

    Google Scholar 

  24. Flanagan, C., Qadeer, S.: A type and effect system for atomicity. In: Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation, pp. 338–349. ACM Press, New York (2003)

    Chapter  Google Scholar 

  25. Flanagan, C., Freund, S.N.: Atomizer: a dynamic atomicity checker for multithreaded programs. In: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 256–267. ACM Press, New York (2004)

    Chapter  Google Scholar 

  26. Saltzer, J.H., Reed, D.P., Clark, D.D.: End-to-end arguments in system design. ACM Transactions on Computer Systems 2, 277–288 (1984)

    Article  Google Scholar 

  27. Flanagan, C.: Verifying commit-atomicity using model-checking. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 252–266. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  28. Robby, Dwyer, M.B., Hatcliff, J.: Bogor: An extensible and highly-modular model checking framework. In: Proceedings of the 9th European Software Engineering Conference held jointly with the 11th ACM SIGSOFT Symposium on the Foundations of Software Engineering. SIGSOFT Softw. Eng. Notes., vol. 28(5), pp. 267–276. ACM Press, New York (2003)

    Google Scholar 

  29. Hartley, S.: Concurrent Programming - The Java Programming Language. Oxford University Press, Oxford (1998)

    Google Scholar 

  30. Jacobs, B., Leino, K.R.M., Schulte, W.: Verification of multithreaded object-oriented programs with invariants. In: Proceedings of The ACM SIGSOFT Workshop on Specification and Verification of Component Based Systems. ACM Press, New York (2004) (to appear)

    Google Scholar 

  31. Ábrahám, E., de Boer, F.S., de Roever, W.P., Steffen, M.: A tool-supported proof system for multithreaded java. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol. 2852, pp. 1–32. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  32. Freund, S.N., Qadeer, S.: Checking concise specifications for multithreaded software. Journal of Object Technology 3, 81–101 (2004)

    Article  Google Scholar 

  33. Wang, L., Stoller, S.D.: Run-time analysis for atomicity. In: Proceedings of the Third Workshop on Runtime Verification (RV). Electronic Notes in Theoretical Computer Science, vol. 89(2). Elsevier, Amsterdam (2003)

    Google Scholar 

  34. Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property specification patterns for finite-state verification. In: Proceedings of the Second Workshop on Formal Methods in Software Practice, pp. 7–15 (1998)

    Google Scholar 

  35. Corbett, J.C., Dwyer, M.B., Hatcliff, J.: Expressing checkable properties of dynamic systems: The Bandera Specification Language. In: International Journal on Software Tools for Technology Transfer, vol. 4, pp. 34–56 (2002)

    Google Scholar 

  36. Deng, X., Dwyer, M.B., Hatcliff, J., Mizuno, M.: Invariant-based specification, synthesis, and verification of synchronization in concurrent programs. In: Proceedings of the 24th International Conference on Software Engineering (ICSE 2002), pp. 442–452. ACM Press, New York (2002)

    Chapter  Google Scholar 

  37. Cheon, Y., Leavens, G.T.: A runtime assertion checker for the Java Modeling Language (JML). In: Proceedings of The International Conference on Software Engineering Research and Practice, June 2002, pp. 322–328. CSREA Press (2002)

    Google Scholar 

  38. SAnToS: JMLEclipse Website (2004), http://jmleclipse.projects.cis.ksu.edu

  39. Burdy, L., Requet, A., Lanet, J.L.: Java applet correctness: A developer-oriented approach. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 422–439. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computing and Information Sciences, Kansas State University,  

    Edwin Rodríguez, John Hatcliff &  Robby

  2. Department of Computer Science and Engineering, University of Nebraska-Lincoln,  

    Matthew Dwyer

  3. Computer Science Department, University of California, Santa Cruz

    Cormac Flanagan

  4. Department of Computer Science, Iowa State University,  

    Gary T. Leavens

Authors
  1. Edwin Rodríguez
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Matthew Dwyer
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Cormac Flanagan
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. John Hatcliff
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Gary T. Leavens
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Robby
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Portland State University,  

    Andrew P. Black

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Rodríguez, E., Dwyer, M., Flanagan, C., Hatcliff, J., Leavens, G.T., Robby (2005). Extending JML for Modular Specification and Verification of Multi-threaded Programs. In: Black, A.P. (eds) ECOOP 2005 - Object-Oriented Programming. ECOOP 2005. Lecture Notes in Computer Science, vol 3586. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11531142_24

Download citation

  • DOI: https://doi.org/10.1007/11531142_24

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-27992-1

  • Online ISBN: 978-3-540-31725-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation