A Petri net semantics for B(PN)2 with procedures

Verification of parallel programs is a very important goal on the way to improve the reliability of software. The PEP tool, a programming environment based on Petri nets, allows verification of parallel programs by a variety of different verification methods (e.g., partial order or BDD based model checking, and stubborn set or symmetrically reduced state space analysis) based on a compositional denotational Petri net semantics. The main contribution of this paper consists in the development of a fully compositional high-level Petri net semantics for concurrent programs with procedures, covering recursion, global variables, and different types of parameter passing (including call-by-reference). The semantics (which is already implemented) is oriented towards verification, i.e., the semantic models are minimised. Due to the abstract and flexible nature of the Petri net model used, our approach is very general and may also be applied to other specification and programming languages. We are, for instance, presently approaching SDL (Specification and Description Language)