Arcadia Papers: ABSTRACT
Arcadia Papers: ABSTRACTState 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.