In: Lecture Notes in Computer Science, Vol. 1217: Proceedings of TACAS'97 (Tools and Algorithms for the Construction and Analysis of Systems), Enschede, pages 65-80. Springer-Verlag, March 1997. Available at http://www.informatik.uni-hildesheim.de/~pep.
Abstract: The PEP tool is a Programming Environment based on Petri Nets. Sophisticated programming and verification components are embedded in a user-friendly graphical interface. The basic idea is that the programming component allows the user to design concurrent algorithms in an easy-to-use imperative language, and that the PEP system then generates Petri nets from such programs in order to use Petri net theory for simulation and verification purposes.
The main focus of this paper is the reference component which represents the bridge between these two worlds. We integrate references in the formal semantics and present some of the provided features. Among others the simulation of a parallel program can be triggered through the simulation of a Petri net. Program formulae can be transformed automatically into net formulae which can then be an input for the verification component.
PEP has been implemented on Solaris 2.x, Sun OS 4.1.x and Linux. Ftp-able versions are available via www.informatik.uni-hildesheim.de/~pep.
Keywords: B(PN)2; Model checking; Parallel finite automata; PEP; Petri nets; Reference component; Simulation; Temporal logic; Tool.