The PEP tool can be considered to be one of the most widely distributed Petri net based tools. A continuously increasing functionality and an adequate graphical user interface may have been good reasons for its acceptance. Currently the tool contains approximately 500,000 lines of source code, and supports (to the best of our knowledge) the widest variety of input formalisms and verification methods of all verification tools. We briefly review the most recent developments.
Ftp-able versions of the tool and PEP related papers are available via http://theoretica.informatik.uni-oldenburg.de/~pep.
Keywords: 3D visualisation, C code generation, Parallel programs, PEP, Petri nets, SDL, Simulation, Verification.This paper describes how the PEP tool (Programming Environmnet based on Petri nets) profits from an integration of the Spin (Simple PROMELA INterpreter) verification package.
Translation methods from three input formalisms (parallel programs, high-level and low-level Petri nets) into PROMELA (PROtocol MEta LAnguage) are discussed and the Spin based verification is compared with a Petri net based partial order model checker using a number of typical examples.
Keywords: Parallel programs, PEP, Petri nets, PROMELA, SDL, Spin, Verification.In this paper a compositional high-level Petri net semantics for SDL (Specification and Description Language) is presented. Emphasis is laid on the modelling of dynamic creation and termination of processes and of procedures - features, which are, for instance, essential for typical client-server systems.
In a preliminary paper we have already shown that we are able to use `state of the art' verification techniques by basing our approach on M-nets (an algebra of high-level Petri nets). Therefore, this paper concentrates on the details of the semantics.
A distinctive feature of the presented solution is that the `infinite case' (infinitely many concurrent process and procedure instances as well as unbounded capacities of input queues and channels) is covered.
Keywords: ARQ protocol, Compositionality, Concurrency, Dynamic Processes, Infinity, Petri Net Semantics, Procedures, SDL.This paper introduces a method to combine finite automata, parallel programs and SDL (Specification and Description Language) specifications. We base our approach on M-nets exploiting the rich set of composition operators available in this algebra of high-level Petri nets. In order to be able to combine different modelling techniques, we rely on compatible interfaces. Therefore,
In this paper, a new method for proving qualitative properties of SDL-systems is presented, which is based on a compositional high-level Petri net semantics for SDL. Since emphasis is laid on the modelling of dynamic creation and termination of processes and of procedures, our method is especially interesting for typical client-server systems.
By using M-nets as the semantic model we are able to use `state of the art' verification techniques. For instance, the verification component of the PEP tool may be applied which presently includes partial order based model checking and algorithms based on linear programming as well as interfaces to other verification packages such as INA, SMV and SPIN providing reduction algorithms based on BDDs, on the stubborn set or sleep set method, and on symmetries.
We show the benefits of our method applying it to a typical client-server system. After describing how safety, liveness and progress properties can be checked fully automatically, we give examples how the compositional nature of the M-net semantics can be used to solve the `state explosion' problem, and how interactive verification may extend the verification possibilities.
Keywords: Compositionality, Concurrency, Dynamic Processes, Petri Net Semantics, Procedures, SDL, Verification.In this paper a high-level Petri net semantics for SDL (Specification and Description Language) is presented. Emphasis is laid on the modelling of dynamic creation and termination of processes and of procedures - features, which are, for instance, essential for typical client-server systems.
In addition to presenting the main ideas as well as the details of the semantics, we show that we are able to use `state of the art' verification techniques by basing our approach on M-nets (an algebra of high-level Petri nets). Therefore, we verify our running example, an ARQ (Automatic Repeat reQuest) communication protocol, using the verification component of the PEP tool which presently includes partial order based model checking and algorithms based on linear programming as well as interfaces to other verification packages such as INA, SMV and SPIN providing reduction algorithms based on BDDs, on the stubborn set or sleep set method, and on symmetries. Moreover, we give examples how the compositional nature of the M-net semantics can be used to solve the `state explosion' problem, and how interactive verification may extend the verification possibilities.
Keywords: ARQ protocol, Compositionality, Concurrency, Dynamic Processes, PEP tool, Petri Net Semantics, Procedures, SDL, Verification.The PEP tool is a Programming Environment based on Petri Nets. Comprehensive modelling, compilation, simulation and verification components are embedded in a user-friendly graphical interface. The basic idea is that the modelling component allows the user to design parallel systems by parallel finite automata, parallel programs, process algebra terms, high-level or low-level Petri nets, and that the PEP system then automatically generates Petri nets from such models in order to use Petri net theory for simulation and verification purposes.
This paper describes the typical usage of the PEP tool by considering the design of the well-known `alternating-bit' protocol. Among others, the usefulness of new concepts for the handling of hierarchies and synchronous communication is explained.
PEP has been implemented on Solaris 2.x and Linux. Ftp-able versions are available via http://parsys.informatik.uni-oldenburg.de/~pep.
Keywords: `Alternating bit' protocol, B(PN)^2, Hierarchical Petri nets, M-nets, Parallel finite automata, Parallel programs, PEP, Simulation, Tool, Verification.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 and Linux. Ftp-able versions are available via http://parsys.informatik.uni-oldenburg.de/~pep.
Keywords: Binary decision diagrams, B(PN)^2, Model checking, PEP, Petri nets, Simulation, Stubborn sets, Temporal logic, Tool.It is commonly known that every reachable marking of a finite-state Petri net system is represented in its finite unfolding according to McMillan. Also the reachability of markings from each other is represented in the finite unfolding, but it is almost unknown that this information can be hidden very deep. This paper presents an efficient method for gaining this information, which is of course of great importance for potential modelcheckers working on finite unfoldings. All results presented in this paper also hold for a recently proposed optimized unfolding method.
Keywords: Branching process, Finite unfolding, Model checking, Petri net, Reachability of markings, Tricky events, Verification.Verification of parallel programs is a very important goal on the way to improve the reliability of software. The PEP tool, a Programming Environment based on Petri nets, allows verification of parallel programs by a variety of different verification methods (e.g., partial order or BDD based model checking, and stubborn set or symmetrically reduced state space analysis) based on a compositional denotational Petri net semantics.
The main contribution of this paper consists in the development of a fully compositional high-level Petri net semantics for concurrent programs with procedures, covering recursion, global variables, and different types of parameter passing (including call-by-reference). The semantics (which is already implemented) is oriented towards verification, i.e., the semantic models are minimised.
Due to the abstract and flexible nature of the Petri net model used, our approach is very general and may also be applied to other specification and programming languages. We are, for instance, presently approaching SDL (Specification and Description Language).
Keywords: B(PN)^2, High-level Petri Nets, M-nets, Parallel Programming Language, PEP, Petri Net Semantics, Procedures, Verification.The PEP tool is a Programming Environment based on Petri Nets. Sophisticated programming and verification components are embedded in a user-friendly graphical interface. The basic idea is that the programming component allows the user to design concurrent algorithms in an easy-to-use 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.
The main focus of this paper is the reference component which represents the bridge between these two worlds. We integrate references in the formal semantics and present some of the provided features. Among others the simulation of a parallel program can be triggered through the simulation of a Petri net. Program formulae can be transformed automatically into net formulae which can then be an input for the verification component.
PEP has been implemented on Solaris 2.x and Linux. Ftp-able versions are available via http://parsys.informatik.uni-oldenburg.de/~pep.
Keywords: B(PN)^2, Model checking, Parallel finite automata, PEP, Petri nets, Reference component, Simulation, Temporal logic, Tool.This paper presents the syntax of a concurrent programming The PEP system (Programming Environment based on Petri Nets) supports the most important tasks of a good net tool, including HL and LL net editing and comfortable simulation facilities. In addition, these features are embedded in sophisticated programming and verification components.
The programming component allows the user to design concurrent algorithms in an easy-to-use imperative language, and the PEP system then generates Petri nets from such programs. The PEP tool's comprehensive verification components allow a large range of properties of parallel systems to be checked efficiently on either programs or their corresponding nets. This includes user-defined properties specified by temporal logic formulae as well as specific properties for which dedicated algorithms are available.
PEP has been implemented on Solaris 2.4, SunOS 4.1.3 and Linux. Ftp-able versions are available.
Keywords: B(PN)^2, Model checking, Parallel finite automata, PEP, Petri nets, Process algebra, Temporal logic, Tool.Verification of parallel programs is a very important goal on the way to improve the reliability of software. The PEP tool, a Programming Environment based on Petri nets, allows verification of parallel programs by partial order model checking based on a compositional denotational Petri net semantics.
The language supported by the PEP tool covers block structuring, parallel and sequential composition, choice, iteration, synchronous and asynchronous communication, including use of unbounded buffers. At present, it does not cover, however, the structuring of programs by procedures.
The main contribution of this paper consists in the development of a fully compositional high-level Petri net semantics for concurrent programs with procedures, covering recursion, global variables, and different types of parameter passing (including call-by-reference).
The semantics will guarantee that the
semantical model (high-level as well as low-level net) of program P is finite
whenever:
- P has only finite data types.
- For each procedure in P only finitely many instances can
be active concurrently.
Due to the abstract and flexible nature of the Petri net model used, our approach is very general and may also be applied to other specification and programming languages. This has already partially been done for SDL (Specification and Description Language).
Keywords: B(PN)^2, high-level Petri nets, M-nets, parallel programming language, PEP, Petri net semantics, procedures, verification.