The P-UMLaut tool allows the user to transform UML 2.0 Sequence Diagrams to semantically equivalent Petri Nets. These Petri Nets may then be simulated using the supplied PN simulator (of PEP descent) or operated on with any tool that can work with high level Petri Nets. By plugging different Realms into the simulation by way of an event filter, the modeled world may then be displayed and interacted with in various fashions. A 3D animation module is supplied as well as two examples utilizing the complete toolchain.
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.