PEP is a modeling and verification framework for parallel systems. It provides a large number of different modelling languages (e.g. SDL, B(PN)^2, Petri nets, Process algebras and Finite Automata), and verification techniques (e.g. reachability and temporal logic model checking). Due to its Tcl/Tk-based GUI, PEP is easily extensible to other analysis or specification tools. The framework offers fully integrated simulation and debugging features on all levels.