In: Lecture Notes in Computer Science, Vol. 1254: Proceedings of CAV'97 (Computer Aided Verification), Haifa, pages 440-443. Springer-Verlag, June 1997. Available at http://www.informatik.uni-hildesheim.de/~pep.
Abstract: The PEP tool embeds sophisticated programming and verification components in a user-friendly graphical interface. The basic idea is that the programming component allows the user to design concurrent algorithms in an 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. A key feature is flexibility; its modular design eases the task of adding new interfaces to other verification packages, such as `INA', `PROD' or `SMV'.
PEP has been implemented on Solaris 2.x, Sun OS 4.1.x and Linux. Ftp-able versions are available via http://www.informatik.uni-hildesheim.de/~pep.
Keywords: Binary decision diagrams; B(PN)²; Model checking; PEP; Petri nets; Simulation; Stubborn sets; Temporal logic; Tool.