The PEP tool (Programming Environment based on Petri Nets) is a comprehensive
set of modelling, compilation, simulation and verification components, linked
together within a Tcl/Tk-based graphical user interface.
- PEP's modelling components facilitate the design of parallel systems by
parallel programs (B(PN)^2 and SDL), interacting finite automata, process
algebra, or high-level/low-level Petri nets.
- PEP's compilers generate Petri nets from such models.
- PEP's simulators allow automatic or user-driven simulation of high-level /
low-level nets and may trigger simulation of the corresponding programs
and/or a 3D model.
- PEP's verification component contains various Petri net indigenous
algorithms to check, e.g., reachability properties and deadlock-freeness,
as well as verification algorithms.
We mention Esparza's partial order based model checker, and interfaces to
- the INA
package (offering structural analysis - invariants, etc. - as well
as stubborn set and symmetrically reduced state space analysis),
- the FC2Tools
(offering verification based on networks of automata),
(offering BDD based CTL model checking) and
(offering LTL model checking with optional partial order reductions).
- The PEP tool can be considered as an open platform.
Further algorithms can be integrated in the user interface easily.
PEP is now hosted at SourceForge!
Christian Stehno email@example.com, 27.10.2004