Formal specification of Java concurrency to assist software verification

The Java programming language is a modem object-oriented language that supports concurrency. Ensuring concurrent programs are correct is difficult. Additional problems encountered in concurrent programs, compared with sequential programs, include deadlock, livelock, starvation, and dormancy. Often these problems are related and are sometimes side effects of one another Furthermore, different programming languages attach different meanings to these terms. Sun Microsystems provides a textual description of the Java concurrency model which is inadequate for reasoning with such programs. Formal specifications are required for verifying concurrent programs through the use of tools and methods such as static analysis, dynamic analysis, model-checking, and theorem proving. It is clear that the behaviour of the Java concurrency model must be unambiguous and well-understood for these tools to operate effectively. This paper presents a formal specification of the Java concurrency model using the Z specification language. A number of important correctness properties of concurrent programs are constructed from the model, and their application to the implementation of verification and testing tools for concurrent Java programs is discussed.