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.


Year:
2004
Keywords:
Laboratories:




 Record created 2005-07-13, last modified 2018-03-17


Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)