A Framework for Model Checking Concurrent Java Components

摘要

The Java programming language supports concurrency.Concurrent programs are harder to verify thantheir sequential counterparts due to their inherent nondeterminismand a number of specific concurrency problems,such as interference and deadlock. In this paper weillustrate how to construct a base model of Java concurrencyprimitives 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 ofusing SPIN for verifying concurrent Java components. Thisbuilds on previous work and contributes in three ways, 1)each Java concurrency primitive is modelled directly andadded to a standard modelling library for inclusion intomodels for a range of concurrent components, 2) we assumea concurrent component may be used in potentially manycontexts rather than simply the context or contexts it mayhave been used or found, 3) by providing a modelling librarywe illustrate how model checking can be implemented in asimple, powerful, and practical manner.