Tool Exhibition

An exhibition of Petri net tools will take place on Wednesday, after “Session C: Tools”, from 17:00 to 18:00, in the lobby of Building IV. The exhibition consists of informal demonstrations for small groups/individuals and there are no scheduled talks. Before the exhibition, at the end of the “Session C: Tools”, in Room 204 of Building IV, there will be a 3-minute presentation about each tool.

The following tools will be part of the tool exhibition.

CosyVerif 

Presenters: Van-François LE, Jaime ARIAS
URL of the Cosyverif: www.cosyverif.org
URL of the Demo CosyDraw: https://cosyverif.lipn.univ-paris13.fr/
Description: CosyVerif is an open source software environment whose goal is the formal specification and verification of dynamic systems. This environment consists of two software tools: CosyDraw, the graphical web interface; and Alligator, an integration framework web service. On one hand, Alligator supports several verification tools, for instance, COSMOS, IMITATOR, GreatSPN, among others. Additionally, it offers the possibility to integrate new tools easily. On the other hand, CosyDraw provides a user friendly graphical interface to draw models for formalisms defined with the Formalism Markup Language (FML – http://www.cosyverif.org/documentation/). CosyDraw is built using cutting-edge web technologies, thus users can start to design models only by opening their preferred browser on any operating system (Windows, OSX, GNU/Linux) and device (smartphones, tablets, laptops). CosyDraw allows to consume services offered by any Alligator instance, allowing users to host their own server with their own tools. Moreover, models can be saved and shared using the Graph Markup Language (GrML). Finally, CosyVerif handles user accounts, providing users with their own private space for saving models and servers. CosyVerif is a software that is actively maintained by the French laboratories LIP6, LIPN, and LMF. Moreover, it has been used for several industrial case studies and for teaching at university.”

Mochy

Presenters: Antoine THEBAULT, Loïc HELOUET
URL of the tool: https://adt-mochy.gitlabpages.inria.fr/mochy/
Description: MOCHY is a tool for the analysis of concurrent stochastic and hybrid systems. It allows for the fast design of timed and stochastic variants of Petri nets, fast simulation of models, and measure of statistics for user-definable values.

TINA toolbox

Presenter: Silvano Dal Zilio, CNRS
URL of the tool: https://projects.laas.fr/tina
Description: TINA (the TIme petri Net Analyzer) is a toolbox for the edition and analysis of Petri Nets and its extensions: inhibitor and read arcs; Time Petri Nets; priorities and stopwatches; and an extension of Time Petri Nets with data handling called Time Transition Systems.

Hippo-CPS

Presenter: Remigiusz Wisniewski
URL of the former tool: http://www.hippo.uz.zgora.pl
URL of the currently under development tool: https://hippo-cps.issi.uz.zgora.pl
Description: Hippo-CPS is a tool that supports the analysis and design of Petri net-based cyber-physical systems. The tool offers the set of verification and design modules of the CPS, including examination of its main properties (such as liveness, boundedness, and safeness), as well as the performance of advanced concurrency and sequentiality analysis of the system (including state-space analysis, place invariant analysis, state machine component-based analysis, etc.). The main aim of the tool is the possibility of alternate analysis/design of the system in regard to the efficiency (run-time) and effectiveness (proper results) of the techniques.

I Love Petri Nets

Presenters: Robin Bergenthum, Jakub Kovar, Sabine Folz-Weinstein
URL of the tool: https://www.fernuni-hagen.de/ilovepetrinets/
Description: I Love Petri Nets is a web toolkit with a collection of Petri net algorithms. Two related papers are presented at the main conference: ILP² Miner – Process Discovery for Partially Ordered Event Logs using Integer Linear Programming and Token Trail Semantics – Modeling Behavior of Petri Nets with Labeled Petri Nets. Both, the “ILP² Miner” and the “Token Trail“ plugin are implemented in the I Petri Nets web toolkit at ILP² Miner: https://www.fernuni-hagen.de/ilovepetrinets/shark/index.html and Token Trails: https://www.fernuni-hagen.de/ilovepetrinets/fox/index.html

Explorative Process Discovery using Activity Projections

Presenter: Yisong Zhang
URL of the tool: https://promtools.org/
Description: EPD-Tool aims at exploring quality changes after removing activities from an event log. The main idea is to create a projected event log for every non-empty subset of activities and apply process discovery and conformance checking on them. The tool has been implemented as a plugin in ProM. First, EPD-Tool uses a process discovery algorithm to discover Petri net models for each projected event log. Then, EPD-Tool uses a conformance checking technique to compute conformance measures for each projected event log and model pair (L,N), e.g., fitness, precision, and F_1-score. Finally, a dendrogram is generated to visualize the relationship between each log-model pair, thus enabling the systematic exploration of the different models using the dendrogram to find the best-performing node, i.e., a best log-model pair. This method prioritizes activities and detects redundancy in the process, which contributes to process enhancement. Conversely, critical activities are uncovered to help to shorten the processing time or save the process cost. To install EPD-Tool, simply download the latest ProM Nightly https://promtools.org, run the PackageManager, select the package “ExplorativeProcessDiscovery”, and run ProM.

Data-Aware Stochastic Processes – Discovery and Conformance Checking

Presenter: Felix Mannhardt
URL of the tool: https://svn.win.tue.nl/repos/prom/Packages/StochasticLabelledDataPetriNet/
Description: The conformance checking and discovery methods presented in (https://link.springer.com/chapter/10.1007/978-3-031-33620-1_5#Sec13) are implemented as plug-ins of ProM in the StochasticLabelledDataPetriNet package. The discovery plug-in first uses the alignments provided by ProM to obtain the observation instances, after which the logistic regression implementation provided by Weka 3.8 based on ridge regression is leveraged for inferring the weight function. A parameter adjusts the one-hot encoding for categorical event log attributes: it sets a maximum on the number of categories that are considered for one-hot encoding for a single variable. Another parameter avoids using one-hot encoding altogether and only considers numerical variables. This is useful to avoid attempting to create a model with a very large number of variables which poses the risk of over-fitting and excessive run times. The conformance checking plug-in implements duEMSC, by extending the EarthMoversStochasticConformance implementation.

IOPT-Tools

Presenter: Luis Gomes, Fernando Pereira, Filipe Moutinho
URL of the tool: https://gres.uninova.pt/IOPT-Tools/
Description: The IOPT-Tools cloud-based tool-chain offers a complete set of tools supporting design automation for embedded controller’s development, benefiting from adopting a model-driven development attitude. The tools are freely available online at http://gres.uninova.pt/IOPT-Tools/. The tool-chain relies on IOPT nets (Input-Output Place-Transition nets) to describe the controller behavior, allowing an explicit representation of constraints on input and output signals and events, which is necessary for the development of controllers. The IOPT-Tools tool-chain includes tools for interactive graphical IOPT nets models editing, simulation and test (token-player, timing diagram, remote debugging), as well as a state-space generator, state-space visualization, and a query system for properties verification. The tool-chain also supports the automatic generation of execution code to be directly deployed in the controllers’ implementation platforms, such as FPGA boards, as well as Arduino, Raspberry, and other Linux-based boards. Most notably, it is possible to obtain C code and VHDL code to be directly deployed into the referred boards without writing/changing a line in the generated code. The tool-chain uses the PNML format for storing the models and can import PNML models generated by other frameworks, automatically generating, if necessary, an associated graphical representation. After, it is possible to add input and output signals and events to create controller models. IOPT-Tools also support net operations, namely net addition, allowing composition of sub-models, and net splitting, which in conjunction with the use of clock domains and dedicated communication channels support the development of distributed controllers.

Renew (Reference Net Workshop)

Presenters: Daniel Moldt (present); Laif-Oke Clasen, Marcel Hansson, Lukas Seifert, Karl Ihlenfeldt, Kjell Ehlers, and more (online).
URL of the tool: http://www.renew.de
Description: Renew is a tool to model and simulate various kinds of Petri nets, especially reference nets. In addition, its plugin architecture allows to extend Renew with your own plugins to extend the functionality. The source code of all stable components of Renew is available via the website. Also some experimental plugins are available. Renew is currently one of the few tools of non trivial size that was transformed from its former 1.6/1.8 Java code base towards the JPMS (Java Platfom Module System) Java 11 / Java 17. The current architecture provides a one plugin = one module = one layer approach allowing to load and unload unused code in Java at runtime.