EUROMICRO Conference (2007)
Aug. 28, 2007 to Aug. 31, 2007
Pavel Parizek , Charles University
Frantisek Plasil , Charles University
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 mitigates 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 to reduce parallelism in the calling protocol on the basis of the information provided by static analysis searching for concurrency-related patterns in the component code; by a heuristic, some of the pattern instances are denoted as "suspicious". Then, the environment (needed to be available since Java PathFinder checks only complete programs) is generated from a reduced calling protocol so that it exercises in parallel only those parts of the component?s code that likely contain concurrency errors.
software components, model checking, concurrency errors, Java PathFinder, static analysis
F. Plasil and P. Parizek, "Partial Verification of Software Components: Heuristics for Environment Construction," EUROMICRO '07. 2007 33rd Euromicro Conference on Software Engineering and Advanced Applications(EUROMICRO), Lubeck, 2007, pp. 75-82.