loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
33rd EUROMICRO Conference on Software Engineering and Advanced Applications (EUROMICRO 2007)
Partial Verification of Software Components: Heuristics for Environment Construction
Lubeck, Germany
August 28-August 31
ISBN: 0-7695-2977-1
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.
Index Terms:
software components, model checking, concurrency errors, Java PathFinder, static analysis
Citation:
Pavel Parizek, Frantisek Plasil, "Partial Verification of Software Components: Heuristics for Environment Construction," euromicro, pp.75-82, 33rd EUROMICRO Conference on Software Engineering and Advanced Applications (EUROMICRO 2007), 2007
Usage of this product signifies your acceptance of the Terms of Use.