Comparing the cost-effectiveness of statically analysing and model checking concurrent java components for deadlocks

Ngui, J., Strooper, P. A., Wildman, L. and Wojcicki, M. (2007). Comparing the cost-effectiveness of statically analysing and model checking concurrent java components for deadlocks. In: J. Grundy and J. Han, Proceedings of the 2007 Australian Software Engineering Conference (ASWEC '07). 18th Australian Conference on Software Engineeing (ASWEC '07), Melbourne, Australia, (223-232). 10-13 April 2007. doi:10.1109/ASWEC.2007.16


Author Ngui, J.
Strooper, P. A.
Wildman, L.
Wojcicki, M.
Title of paper Comparing the cost-effectiveness of statically analysing and model checking concurrent java components for deadlocks
Conference name 18th Australian Conference on Software Engineeing (ASWEC '07)
Conference location Melbourne, Australia
Conference dates 10-13 April 2007
Convener Australian Computer Society & Engineers Australia
Proceedings title Proceedings of the 2007 Australian Software Engineering Conference (ASWEC '07)
Journal name 2007 Australian Software Engineering Conference, Proceedings
Place of Publication Los Alamitos, CA, U.S.A.
Publisher IEEE - Computer Society
Publication Year 2007
Sub-type Fully published paper
DOI 10.1109/ASWEC.2007.16
ISBN 0-7695-2778-7
ISSN 1530-0803
Editor J. Grundy
J. Han
Start page 223
End page 232
Total pages 10
Collection year 2008
Language eng
Abstract/Summary Verifying concurrent Java programs is difficult due to the many possible interleavings of threads and a number of specific concurrency defects such as interference and deadlock. To verify concurrent Java components, the TestCon method combines code inspection, static analysis and dynamic analysis. The deadlock detection steps of TestCon include static analysis (using Jlint) that may result in false positives or false negatives; therefore code inspection is combined with Jlint, but inspection can be time-consuming and depends on the inspector's skills. In this paper, we evaluate the cost-effectiveness of the Java PathFinder 2 (JPF 2) model checker for the detection of deadlocks in the context of the TestCon method. The results of the study show that using JPF 2 can improve TestCon's effectiveness but a trade-off has to be made in terms of cost in the development of the driver and analysis of its output. General conclusions cannot be drawn since the study was exploratory and small-scale; however the observations highlight some of the strengths and weaknesses of using JPF 2 compared to static analysis and code inspection.
Subjects 280302 Software Engineering
700102 Application tools and system utilities
E1
Keyword Java PathFinder 2
Code inspection
Multithreading
Static analysis
Q-Index Code E1
Q-Index Status Confirmed Code

 
Versions
Version Filter Type
Citation counts: TR Web of Science Citation Count  Cited 0 times in Thomson Reuters Web of Science Article
Scopus Citation Count Cited 2 times in Scopus Article | Citations
Google Scholar Search Google Scholar
Created: Thu, 10 Apr 2008, 16:12:50 EST by Donna Clark on behalf of School of Information Technol and Elec Engineering