96): Technical Report (21, pages 1-16 pp.. University of Hildesheim, July 1996. Available at http://www.informatik.uni-hildesheim.de/~pep.
Abstract: 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 partial order model checking based on a compositional denotational Petri net semantics.
The language supported by the PEP tool covers block structuring, parallel and sequential composition, choice, iteration, synchronous and asynchronous communication, including use of unbounded buffers. At present, it does not cover, however, the structuring of programs by procedures.
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 many types of parameter passing (including call-by-reference). The semantics will guarantee that the semantical model of program P is finite whenever: - P has only finite data types. - For each procedure in P only finitely many instances can be active concurrently. 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. This has already (partially) been done for the Specification and Description Language (SDL).
Keywords: B(PN)²; high-level Petri nets; M-nets; parallel programming language; PEP; Petri net semantics procedures; verification.