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.