Programming Environment based on Petri Nets (PEP)

Category Cross-Omics>Agent-Based Modeling/Simulation/Tools

Abstract The PEP tool (Programming Environment based on Petri Nets) is a comprehensive set of modeling, compilation, simulation and verification components, linked together within a “Tcl/Tk-based” graphical user interface.

Tcl (Tool Command Language) is a very advanced but easy to learn dynamic ‘programming language’, suitable for a very wide range of uses, including web and desktop applications, networking, administration, testing and many more.

Open source and business-friendly, Tcl is a mature yet evolving language that is truly ‘cross platform’, easily deployed and highly extensible.

Tk is a Graphical User Interface (GUI) toolkit that takes developing desktop applications to a higher level than conventional approaches.

Tk is the standard GUI Not only for Tcl, but for many other dynamic languages, and can produce rich, native applications that run unchanged across Windows, Mac OS X, Linux and more.

PEP supports the most important tasks of a good net tool, including high-level and low-level net editing with comfortable simulation facilities.

In addition, Petri net editing and simulation is 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 simulation of a Petri net can even trigger the simulation of the corresponding program.

The PEP tool’s comprehensive verification components allow the analysis of a large range of properties of ‘parallel systems’ which can 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 have been implemented.

PEP has been created for the development, verification, and simulation of ‘parallel programs’.

The structure of the PEP tool consists of three (3) levels:

1) At the development level user input is accepted in the form of programs written in one of the languages B(PN)^2 and SDL or as a ‘parallel finite automata’.

2) At the net level, specifications are represented as ‘high level nets’, ‘Petri box calculus’ expressions, and low-level Petri nets.

‘M-nets’ represent the high level nets and safe2 Petri nets the low-level Petri nets.

3) At the analysis level, ‘model checking’ and other verification methods can be applied to the low-level Petri nets.

PEP’s ‘modeling components’ facilitate the design of parallel systems by parallel programs [B(PN)^2 - a Basic Petri Net Programming Notation and/or the Specification and Description Language (SDL)...], interacting finite automata, process algebra, or high-level/low-level Petri nets.

PEP’s compilers generate Petri nets from such models.

PEP’s simulators allow automatic or user-driven simulation of high-level / low-level nets and may trigger ‘simulation’ of the corresponding programs and/or a 3D model.

PEP’s ‘verification component’ contains various Petri net indigenous algorithms to check, e.g., reachability properties and deadlock-freeness, as well as verification algorithms and Esparza's partial order based model checker.

PEP interfaces to:

1) The Integrated Net Analyzer (INA) package (see G6G Abstract Number 20608) - (offering structural analysis - invariants, etc. - as well as stubborn set and symmetrically reduced state space analysis).

2) The FC2Tools (offering verification based on networks of automata) - The FC2Tools package, together with its graphical editor ‘Autograph’, is a forerunner amongst software dealing with model-based, automatic verification of distributed communicating systems.

FC2Tools ‘main features’ are: implementation of ‘process algebra’ theory, for syntax and semantics; verification by compositional reductions and abstraction;

alternative or combined use of explicit and implicit (BDD) implementation styles for better efficiency; use of the specific ‘FC2 file exchange’ format for easy interface with other verification software.

3) SMV (offering BDD based CTL model checking) - The Symbolic Model Verifier (SMV) system is a tool for checking ‘finite state systems’ against specifications in the temporal logic CTL (Computation Tree Logic).

4) SPIN (offering LTL model checking with optional partial order reductions) - SPIN targets efficient ‘software verification’. The tool supports a high level language to specify ‘systems descriptions’, called PROMELA (a PROcess MEta LAnguage).

SPIN can be used as a full ‘LTL model checking’ system, supporting all correctness requirements expressible in ‘linear time temporal logic’, but it can also be used as an efficient ‘on-the-fly’ verifier for more basic safety and liveness properties.

Many of the latter properties can be expressed, and verified, without the use of LTL.

Correctness properties can be specified as system or process invariants (using assertions), as linear temporal logic requirements (LTL), as formal ‘Büchi Automata’, or more broadly as general ‘omega-regular’ properties in the syntax of ‘never’ claims.

The PEP tool can be considered an open platform. Further algorithms can be easily integrated into its user interface.

System Requirements

PEP has been implemented on Solaris, Linux, Windows (using Cygwin), MacOS X, FreeBSD and other systems.

Manufacturer

Manufacturer Web Site Programming Environment based on Petri Nets (PEP)

Price Contact manufacturer.

G6G Abstract Number 20609

G6G Manufacturer Number 104209