Implementing a State Space Analyzer for Synchronous Java
In this paper we present a toolset aimed at the analysis of programs written in Java and a new kind of active objects. The toolset detects if the program contains deadlocks and may provide a CCS description along with a labeled transition system of the program. When deadlock is found, the toolset proposes some of the traces that lead the program to deadlock status. The analysis tool also translates the generated labeled transition system to the syntax of SMV input language in order to perform the model checking function.