Controlling state explosion in reachability analysis

Concurrent software systems are more difficult to design and analyze than sequential systems. Considerable research has been done to help the testing, analysis, and verification of concurrent systems. Reachability analysis is a family of analysis techniques involving exhaustive examination of the whole state space. Reachability analysis is attractive because it is simple and relatively straightforward to automate, and can be used in conjunction with model-checking procedures to check for application-specific as well as general properties like freedom from deadlocks and race conditions. However, practical application of reachability analysis to real systems has been stymied by the state explosion problem, an exponential growth in the number of states to be explored as the number of processes increases. State explosion can be substantially controlled if the analysis approach is compositional. An analysis technique is compositional if the results of analyzing sub-systems can be composed to obtain analysis results for the complete system. We propose using process algebra to achieve this goal in automated analysis tools. The algebraic structure of process algebra and its rich abstraction capabilities provide the means to achieve compositional (divide-and-conquer) analysis. The primary contribution of this dissertation will be a demonstration and evaluation of the usefulness of process algebra in controlling state explosion in reachability analysis of models close to the model of concurrency found in real programs. We propose a two-leveled approach to control state explosion--using process algebra at the coarse-grained level and simplification strategies based on a process-sleep mechanism at the fine-grained level. Although the process algebra-based compositional approach is not guaranteed to solve the state explosion problem, with a suitably modular design that provides good service abstraction, state explosion can be controlled sufficiently for application of reachability analysis to be practical