| Concurrent programming has two main benefits: First, it allows natural solutions to software design problems that are inherently parallel or distributed. Second, concurrent programs offer potentially better efficiency than sequential programs. However, concurrent programming poses many challenges that do not exist in the sequential setting. For instance, the processes in the system may livelock, diverge, or even deadlock.; The Java Remote Method Invocation (RMI) package facilitates the implementation of concurrent applications in which, for instance, the processes reside on different hosts and communicate over the internet. More precisely, it hides the details of network communication. Unfortunately, it does not relieve the programmer from the potential pitfalls of controlling the concurrent access to remote objects. Consequently, RMI applications are prone to the same problems as concurrent programs in general.; To address this problem, this thesis presents an approach, named JCUV (Java to C++ Using Verisoft) that allows Java RMI programs to be analyzed with respect to deadlock, livelock, divergences, and assertion violations. The approach consists of two steps: First, the Java RMI program is translated into an equivalent C++ program using automated source code transformation. Second, the resulting C++ program is analyzed with the state space exploration tool Verisoft. My thesis discusses the details of the transformation and evaluates the approach on a number of small examples. |
