STATIC ANALYSIS OF CONCURRENT PROCESSES FOR DYNAMIC PROPERTIES USING PETRI NETS.

A new subclass of Petri Nets is presented called the ″Extended Control Structure Nets″ . The control structure of arbitrarily structured parallel programs can be represented by nets of this class, even if they include operations on general semaphores. First of all, the purely statical structure of the Extended Control Structure Nets is dealt with, i. e. the graph of these nets. It is defined, in which way these nets are recursively generated by a composition of connected state machines which in turn represent the control structure of sequential parts of a parallel program or event variables resp. semaphores. Various properties of these graphs of Extended Control Structure Nets are stated. In addition, some special paths in these graphs are defined which are meaningful in respect to the underlying interpretation and thus are important for the later structural analysis.