In: Margaria, T.; Steffen, B.: Lecture Notes in Computer Science, Vol. 1055; Tools and Algorithms for the Construction and Analysis of Systems, Second Int. Workshop, TACAS'96, Passau, Germany, pages 397-401. Springer-Verlag, March 1996. Available at http://www.informatik.uni-hildesheim.de/~pep.
Abstract: This paper presents the syntax of a concurrent programming tool. The PEP system (Programming Environment based on Petri Nets) supports the most important tasks of a good net tool, including HL and LL net editing and comfortable simulation facilities. In addition, these features are embedded in sophisticated programming and verification components. The programming component allows the user to design concurrent algorithms in an easy-to-use imperative language, and the PEP system then generates Petri nets from such programs. The PEP tool's comprehensive verification components allow a large range of properties of parallel systems to be checked efficiently on either programs or their corresponding nets. This includes user-defined properties specified by temporal logic formulae as well as specific properties for which dedicated algorithms are available. PEP has been implemented on Solaris 2.4, SunOS 4.1.3 and Linux. Ftp-able versions are available.
Keywords: B(PN)²; model checking; parallel finite automata; PEP; petri nets; process algebra; temporal logic; tool.