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
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
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)
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
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)
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
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)
Meyer, B.: Object-oriented Software Construction. Prentice-Hall, Englewood Cliffs (1997)
SAnToS: SpEx Website (2003), http://spex.projects.cis.ksu.edu
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)
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)
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)
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)
Lea, D.: Concurrent Programming in Java, 2nd edn. Addison-Wesley, Reading (2000)
Raghavan, A.D., Leavens, G.T.: Desugaring JML method specifications. Technical Report 00-03d, Iowa State University, Department of Computer Science (2003)
Lerner, R.A.: Specifying Objects of Concurrent Systems. PhD thesis, School of Computer Science, Carnegie Mellon University, TR CMU–CS–91–131 (1991)
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)
Noble, J., Vitek, J., Potter, J.: Flexible alias protection. In: Jul, E. (ed.) ECOOP 1998. LNCS, vol. 1445, pp. 158–185. Springer, Heidelberg (1998)
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+
Borgida, A., Mylopoulos, J., Reiter, R.: On the frame problem in procedure specifications. IEEE Transactions on Software Engineering 21, 785–798 (1995)
Lipton, R.J.: Reduction: a method of proving properties of parallel programs. Communications of the ACM 18, 717–721 (1975)
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)
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)
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)
Dietl, W., Müller, P.: Universes: Lightweight ownership for jml. In: Journal of Object Technology (2005) (to appear)
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)
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)
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)
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)
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)
Hartley, S.: Concurrent Programming - The Java Programming Language. Oxford University Press, Oxford (1998)
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)
Á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)
Freund, S.N., Qadeer, S.: Checking concise specifications for multithreaded software. Journal of Object Technology 3, 81–101 (2004)
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)
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)
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)
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)
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)
SAnToS: JMLEclipse Website (2004), http://jmleclipse.projects.cis.ksu.edu
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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)