A deadlock detection tool for concurrent Java programs
This paper presents some issues related to the design and implementation of a concurrency analysis toot able to detect deadlock situations in Java programs that make use of multithreading mechanisms. An abstract formal model is generated from the Java source using the Java2Spin translator. The model is expressed in the PROMELA language, and the SPIN tool is used to perform its formal analysis, The paper mainly focuses on the design of the Java2Spin translator. A set of experiments, carried out to evaluate the performances of the analysis tool, is also presented. Copyright (C) 1999 John Whey & Sons, Ltd.
deadlock java spin promela formal analysis concurrent programming