Arcadia Papers: ABSTRACT

"Graph Models for Reachability Analysis of Concurrent Programs", by Mauro Pezz`e, Richard N. Taylor, and Michal Young in Technical Report TR-92-27, Department of Information and Computer Science, University of California, Irvine CA 92171-3425, January 1992.


The problem of analyzing concurrent systems has been investigated by many researchers and several solutions have been proposed. Among the proposed techniques, reachability analysis --- systematic enumeration of reachable states in a finite-state model --- is attractive because it is conceptually 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.

One thread of research related to reachability analysis involves extracting models from program texts. This paper shows that the nature of the translation from source code to a modeling formalism is of greater practical importance than the underlying formalism. (With respect to the underlying formalisms we present algorithms for translating Taylor's reduced flowgraph model and Long and Clarke's task interaction graph model into a common labeled flowgraph formalism, and for translating labeled flowgraphs into Petri nets, while preserving the reachability graph structure.)

Features identified as pragmatically important are the representation of internal choice, selection of a dynamic or static matching rule, and the ease of applying reductions. Since combinatorial explosion is the primary impediment to application of reachability analysis, a particular concern in choosing a model is facilitating divide-and-conquer analysis of large programs. Recently, much interest in finite-state verification systems has centered on algebraic theories of concurrency. Algebraic structure can be used to decompose reachability analysis based on a flowgraph model. The semantic equivalence of graph and Petri net based models suggests that one ought to be able to apply a similar strategy for decomposing Petri nets. We show this is indeed possible through application of category theory.


The Arcadia Project <>
Last modified: Thu Jan 27 13:36:13 1995