The PEP tool

  • Bernd Grahlmann
Tool Papers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1254)


The PEP tool embeds sophisticated programming and verification components in a user-friendly graphical interface. The basic idea is that the programming component allows the user to design concurrent algorithms in an imperative language, and that the PEP system then generates Petri nets from such programs in order to use Petri net theory for simulation and verification purposes. A key feature is flexibility; its modular design eases the task of adding new interfaces to other verification packages, such as ‘INA’, ‘PROD’ or ‘SMV’.

PEP has been implemented on Solaris 2.x, Sun OS 4.1.x and Linux. Ftp-able versions are available via


Binary decision diagrams B(PN)2 Model checking PEP Petri nets Simulation Stubborn sets Temporal logic Tool 


  1. 1.
    E. Best. Partial Order Verification with PEP. Proc. of POMIV'96, Princeton.Google Scholar
  2. 2.
    E. Best, R. Devillers and J. G. Hall. The Box Calculus: a New Causal Algebra with Multi-Label Communication. Advances in Petri Nets 92, Springer LNCS 609.Google Scholar
  3. 3.
    E. Best, H. Fleischhack, W. Frcaczak, R. P. Hopkins, H. Klaudel, and E. Pelz. An M-Net Semantics of B(PN)2. Proc. of STRICT'95, Springer.Google Scholar
  4. 4.
    E. Best, H. Fleischhack, W. Frcaczak, R. P. Hopkins, H. Klaudel, and E. Pelz. A Class of Composable High Level Petri Nets. Proc. of ATPN'95.Google Scholar
  5. 5.
    E. Best and B. Grahlmann. PEP: Documentation and User Guide. Universität Hildesheim. Available together with the tool via: Scholar
  6. 6.
    E. Best and R. P. Hopkins. B(PN)2 — a Basic Petri Net Programming Notation. Proc. of PARLE, Springer LNCS 694.Google Scholar
  7. 7.
    R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8), 1986.Google Scholar
  8. 8.
    E. Clarke and K. McMillan and S. Campos and V. Hartonas-Garmhausen. Symbolic Model Checking. Proc. of CAV'96, New Brunswick, Springer LNCS 1102.Google Scholar
  9. 9.
    J. C. Corbett. Evaluating Deadlock Detection Methods for Concurrent Software. Technical report, University of Hawaii at Manoa, 1995.Google Scholar
  10. 10.
    J. Esparza, S. Römer, and W. Vogler. An Improvement of McMillan's Unfolding Algorithm. Proc. of TACAS'96, Springer LNCS 1055.Google Scholar
  11. 11.
    J. Esparza. Model Checking Using Net Unfoldings, 151–195. Number 23 in Science of Computer Programming. ELSEVIER, 1994.Google Scholar
  12. 12.
    H. Fleischhack and B. Grahlmann. A Petri Net Semantics for B(PN) 2 with Procedures. Proc. of PDSE'97, Boston.Google Scholar
  13. 13.
    B. Grahlmann, M. Moeller, and U. Anhalt. A New Interface for the PEP Tool — Parallel Finite Automata. Proc. of 2. AWPN'95.Google Scholar
  14. 14.
    B. Grahlmann. The Reference Component of PEP. Proc. of TACAS'97, Enschede. Springer LNCS 1217.Google Scholar
  15. 15.
    B. Graves. Identification of Specific Processes Contained in McMillan's Finite Unfolding. Submitted.Google Scholar
  16. 16.
    M. Heiner and P. Deussen. Petri Net Based Design and Analysis of Reactive Systems. Proc. of WODES'96, Edinburgh.Google Scholar
  17. 17.
    G. Holzmann and D. Peled. The State of SPIN. Proc. of CAV'96, New Brunswick.Google Scholar
  18. 18.
    L. Jenner. A Low-Level Net Semantics for B(PN)2 with Procedures. In E. Best and H. Fleischhack, editors. PEP: Programming Environment Based on Petri Nets. Hildesheimer Informatik-Berichte 14/95. 1995.Google Scholar
  19. 19.
    J. Lilius and E. Pelz. An M-Net Semantics for B(PN)2 with Procedures. Proc. of ISCIS-XI'96.Google Scholar
  20. 20.
    K. McMillan. A Technique of a State Space Search Based on Unfolding. Formal Methods in System Design 6(1), 1996.Google Scholar
  21. 21.
    P. H. Starke. INA: Integrated Net Analyzer. Handbuch, 1992.Google Scholar
  22. 22.
    T. Thielke. Implementierung eines effizienten Modelchecking-Algorithmus. Petri-Netze im Einsatz für Entwurf und Entwicklung von Informationssystemen, 1993.Google Scholar
  23. 23.
    A. Valmari. Stubborn Sets for Reduced State Space Generation. In APN'90, Springer LNCS 483.Google Scholar
  24. 24.
    K. Varpaaniemi and J. Halme and K. Hiekkanen and T. Pyssysalo. PROD Reference Manual. Technical Report B 13, University of Helsinki, 1995.Google Scholar
  25. 25.
    G. Wimmel. A BDD-based Model Checker for the PEP Tool. Technical Report, University of Newcastle upon Tyne, 1997.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Bernd Grahlmann
    • 1
  1. 1.Institut für InformatikUniversität HildesheimGermany

Personalised recommendations