Petri Nets 2012 & ACSD 2012

• Home
• Events
  • Petri Nets 2012
  • ACSD 2012
  • Workshops [an error occurred while processing this directive]
    • Invited Speakers
    • Accepted Contributions
  • Petri Net Course [an error occurred while processing this directive]
    • Schedule
    • Tutorial 1
    • Tutorial 2
  • Tools Exhibition
  • Contest
• Programme
  • Overview
  • Keynotes
  • Social Programme
  • Session Schedule
  • Accepted Papers
  • Proceedings/Awards
• Travel Information
  • How to reach Hamburg
  • Conference Venue
  • Accommodation
  • Sightseeing
• Registration
• Committees
• Supporters
• Contact
• Impressum

Tools Exhibition

An exhibition of Petri net tools takes place on Thursday. It consists of informal demonstrations for small groups/individuals. There are no scheduled talks. Requests for participation in the tools exhibition must be sent to the Tools Exhibition Chair before June 1, 2012 (see Call for Papers for details). They should include a link to the web pages for the tool (or a short description of the tool). The demonstrators bring their own machines, while the organisers may be requested to give access to the Internet.

Snoopy

http://www-dssz.informatik.tu-cottbus.de/snoopy.html

The tool Snoopy provides a unifying Petri net framework which has particularly many application scenarios in systems and synthetic biology. The framework consists of two levels: uncoloured and coloured. Each level comprises a family of related Petri net classes, sharing structure, but being specialized by their kinetic information. Petri nets of all net classes within one level can be converted into each other, while changing the level involves user-guided folding or automatic unfolding. Models can be hierarchically structured, allowing for the mastering of larger networks. Snoopy supports the simultaneous use of several Petri net classes; the graphical user interface adapts dynamically to the active one. Built-in animation and simulation (depending on the net class) are complemented by export to various analysis tools. Snoopy facilitates the extension by new Petri net classes thanks to its generic design.

Grade/CPNi

http://cpntools.org/gradecpn/start

Grade/CPN is a tool for automatically grading several student assignments using CPN Tools. The tool allows teachers to create a generic base model with an interface intended to be filled out by students. Students fill in the missing parts and this can be tested against a formal specification and other formal requirements and assigned scores based on a configuration set up by the teacher. Grade/CPN provides an overview of the overall scores of all students as well as individual reports for each student with scores and reasons for each score.

CPN Assistant II

https://sites.google.com/site/cpnassistant/

CPN Assistant II is a simulation management tool for CPN Tools (version 3). It allows to prepare, run and manage multiple simulation jobs on a single computer or in a networked environment. For each simulation job a net, a number of simulation runs and transition firings per run and a selection of monitors to be processed can be specified. The simulation jobs are automatically distributed to available computers and run. Data acquired by each of the selected monitors during an execution of given simulation job are merged and stored as a text file at a specified location. Post-processing of the data is possible, too.

PeabraiN

http://webdiis.unizar.es/GISED/?q=tool/peabrain

PeabraiN tool is a collection of PIPE (Platform Independent Petri net Editor) modules for computing bounds, resource optimisation, and other properties on the Petri nets (PNs). Namely, the features supported by PeabraiN are the following:

• Performance Estimation
• Resource Optimisation
• Structural Enabling
• Structural Marking
• Visit Ratio Computation
• SPN Simulation Analysis

QPME

http://qpme.sourceforge.net

QPME (Queueing Petri net Modeling Environment) is an open source tool for stochastic modeling and analysis based on the Queueing Petri Net (QPN) modeling formalism. Queueing Petri Nets are a combination of conventional queueing networks and stochastic Petri nets providing increased expressiveness and thus making it possible to model systems at a higher degree of accuracy. QPME is made of two components: QPE (QPN Editor) and SimQPN (Simulator for QPNs). QPE provides a user-friendly graphical tool for modeling using QPNs based on the Eclipse/GEF framework. SimQPN provides an efficient discrete event simulation engine for QPNs that makes it possible to analyze models of realistically-sized systems. QPME runs on a wide range of platforms including Windows, Linux and Mac OS.

Sequence Chart Studio

http://scstudio.sourceforge.net/

The Sequence Chart Studio (SCStudio) is a user-friendly drawing and verification tool for Message Sequence Charts (MSC). SCStudio supports several checkers that are able to verify properties such as realizability, time consistency, equivalence checking between two MSC diagrams, etc. Some of them are well known, while others are new or nontrivial extensions of existing ones. The graphical front-end is implemented as a Microsoft Visio add-on, whereas the checkers are platform independent. SCStudio is an open source project that provides an open interface for additional modules.

Renew

http://www.renew.de/

Renew is an extensible Petri net IDE that supports the development and execution of object-oriented Petri nets, which include net instances, synchronous channels, and seamless Java integration for easy modelling. Renew is available free of charge including the Java source code.

Anica

http://www.service-technology.org/anica/

Anica reads nets where transitions are partitioned into confidential (H) and public (L). It can check an information flow security property that basically says that an observer cannot infer on the occurrence of H transitions. It does so by translating the problems into a large number of reachability problems which are passed to the LoLA verification tool. It turns out that this approach is significantly more efficient than original methods which investigate that whole state space. The reason is that, for all generated reachability problems, LoLA is able to produce a reduced state space.

LoLA

http://www.service-technology.org/tools/lola/

LoLA is an explicit state space generation tool for place/transition nets that is capable of applying a large number of state space reduction techniques in combination. We will show a re-implemention of LoLA that offers several new features, including

• a new architecture where the user does not need to re-compile LoLA when switching between reduction techniques
• the possibility to monitor LoLA from a distant computer
• the possibility to switch between several marking storage concepts, including hash-based techniques

PAT

http://www.comp.nus.edu.sg/~pat/

PAT (Process Analysis Toolkit) is a self-contained framework that supports the composition, simulation and reasoning of concurrent, real-time systems and other possible domains. It comes with user friendly interfaces, featured model editor and animated simulator. Most importantly, PAT implements various model checking techniques for different properties such as deadlock-freeness, divergence-freeness, reachability, LTL properties with fairness assumptions, refinement checking and probabilistic model checking.

CosyVerif

http://www.cosyverif.org/

CosyVerif is a software environment aiming at formal specification and verification of dynamic and distributed systems. It has been designed in order to:

• support different formalisms with the ability to easily create new ones,
• provide a graphical user interface for every formalism,
• include verification tools called as web services via the interface,
• offer the possibility for developers to integrate their own tools, allowing for interaction with the other tools.

This environment consists of two main software tools: Coloane, the graphical interface, and Alligator, an integration framework based on web services. It is enlarged with the existing verification tools developed in partner laboratories. CosyVerif currently supports automata and Petri nets, both with extensions. It is mainly dedicated to the modelling and analysis of distributed and timed systems.