Comparing the Cost-Effectiveness of Statically Analysing and Model Checking Concurrent Java Components for Deadlocks

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.