A Framework for Model Checking Concurrent Java Components

The Java programming language supports concurrency. Concurrent programs are harder to verify than their sequential counterparts due to their inherent non-determinism and a number of specific concurrency problems, such as interference and deadlock. In this paper, the authors illustrate how to construct a base model of Java concurrency primitives using the Promela language of SPIN. Subsequently, a readers-writers monitor, and eighteen mutants, are used as an example to show the power and simplicity of using SPIN for verifying concurrent Java components.