Abstract
Code model checking of software components suffers from the well-known problem of state explosion when applied to highly parallel components, despite the fact that a single component typically comprises a smaller state space than the whole system. We present a technique that addresses the problem of state explosion in code checking of primitive components with the Java PathFinder in case the checked property is absence of concurrency errors.
The key idea is reduction of parallelism in the environment so that only those parts of the component?s code that can likely cause concurrency errors are exercised in parallel; such parts are identified via a heuristic static code analysis (searching for ?suspicious? patterns in the component code). Benefits of the technique, i.e. support for discovery of concurrency errors in limited time and space and provision of easy-to-read counterexamples, are illustrated on the results of several experiments.