Deadlock Detector for Synchronous Java.

In this paper, we present a work that aims to detect deadlocks in the programs written in the Synchronous Java language (sJava). It is based on an extension to a model-checking framework Bogor that allows the verification of concurrent Java programs. The deadlock detector allows developers to analyze the concurrent interaction of threads of active objects for searching all the reachable states and possible execution paths and detecting any deadlocks presented in a model. We propose in this work a solution that solves the problem of synchronization of method calls between active threads without using the traditional wait-notify mechanism. We also propose a utility that shows the graph of finite state machines of the simple models after verifying using Bogor.