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),
- SMV
(offering BDD based CTL model checking) and
- SPIN
(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!
Back to
Christian Stehno pep_help@informatik.uni-oldenburg.de, 27.10.2004
