Premium
A deadlock detection tool for concurrent Java programs
Author(s) -
Demartini Claudio,
Iosif Radu,
Sisto Riccardo
Publication year - 1999
Publication title -
software: practice and experience
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.437
H-Index - 70
eISSN - 1097-024X
pISSN - 0038-0644
DOI - 10.1002/(sici)1097-024x(199906)29:7<577::aid-spe246>3.0.co;2-v
Subject(s) - computer science , promela , java , programming language , concurrency , deadlock , multithreading , java modeling language , real time java , set (abstract data type) , java concurrency , deadlock prevention algorithms , communicating sequential processes , model checking , java annotation , thread (computing) , semantics (computer science) , operational semantics
This paper presents some issues related to the design and implementation of a concurrency analysis tool 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 © 1999 John Wiley & Sons, Ltd.