Deadlock detection for synchronous Java

The aim of this thesis is to construct toolsets that support the Synchronous Java programming language, an extension to the Java language that introduces a new method of synchronization between threads. The contributions of this thesis include a State Space Analyzer (SSAS) and a Deadlock Detector for Synchronous Java (DDSJ). As the first tool I developed an analyzer, the SSAS, that explores all the reachable states and all the possible execution paths of an sJava model. This exploration aims at the analysis of the communication between active threads and the detection of deadlocks in a given sJava model. When a deadlock is encountered, the toolset generates the error traces that help the developers to examine how the deadlocks were produced in the input model. The analyzer also generates the state space of the system model and a graphical representation of this state space. In the second toolset, the DDSJ, I developed an approach that reduces the number of states when verifying an sJava program in Bandera and Bogor, which are the toolsets that support the verification of Java models. If errors are detected when verifying an sJava model, DDSJ generates a counter-example that allows developers to simulate the execution of the given model to study how errors were produced. The outcomes of this thesis give the Synchronous Java developers more confidence in using this programming language. These toolsets provide a possibility to examine sJava programs and to refine them before they can be delivered as product.