Static Analysis of Java Mutithreaded and Distributed Applications

The Java language enables the development of concurrent and distributed software through the concepts of thread and remote method invocation (RMI). It is known that developing concurrent and distributed software is a challenging task, mainly because of potential concurrency errors such as deadlocks and livelocks. One promising way to help the designer bl this task is providing static analysis tools that can detect such errors in the source code, as documented in the rich literature on static analysis of Ada tasking programs. This paper extends the approach followed for Ada tasking programs to the new Java language, providing formal models for the main thread synchronization primitives offered by the language. The formalism used is Promela, the input language of the model checker SPIN, which is based on extended communicating finite state machines and provides an efficient analysis algorithm.