Parallel Programs as Petri Nets

Simulation, analysis and verification of parallel programs is a major challenge. This thesis proposes a solution which is based on Petri nets. The main contribution is the formal definition of compositional high-level Petri net semantics for B(PN)2 Basic Petri Net Programming Notation) programs and SDL (Specification Description Language) systems. The correct and efficient translation of also recursive procedures (in B(PN)2 and SDL) and processes with dynamic creation and termination (in SDL) into high-level Petri nets are distinguishing characteristics. In addition to the semantics definitions, all related issues are covered: The M-net model, an algebra of high-level Petri nets, is extended in such a way that all coherence and algebraic properties are still fulfilled. References which relate parts of the programs with parts of the resulting nets are formally introduced in the semantics. Implementational aspects and the integration into the PEP tool are described. Examples are given, in particular, to demonstrate how the presented approach supports verification. Finally, the definition of a high-level Petri net semantics for 'hybrid' systems which are composed of B(PN)2 parts, SDL parts and B(PN)2 and/or SDL specific finite automata gives evidence for the general applicability of the presented concepts.