DocumentCode :
2412882
Title :
Comparing the Cost-Effectiveness of Statically Analysing and Model Checking Concurrent Java Components for Deadlocks
Author :
Ngui, John ; Strooper, Paul ; Wildman, Luke ; Wojcicki, Margaret
Author_Institution :
Sch. of Inf. Technol. & Electr. Eng., Queensland Univ., Brisbane, Qld.
fYear :
2007
fDate :
10-13 April 2007
Firstpage :
223
Lastpage :
232
Abstract :
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.
Keywords :
Java; concurrency control; multi-threading; program diagnostics; program verification; Java PathFinder 2; code inspection; concurrent Java program verification; deadlock detection; dynamic analysis; model checking; multithreading; static analysis; Concurrent computing; Context modeling; Costs; Inspection; Interference; Interleaved codes; Java; System recovery; Testing; Yarn;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Software Engineering Conference, 2007. ASWEC 2007. 18th Australian
Conference_Location :
Melbourne, Vic.
ISSN :
1530-0803
Print_ISBN :
0-7695-2778-7
Type :
conf
DOI :
10.1109/ASWEC.2007.16
Filename :
4159675
Link To Document :
بازگشت