NetAnalysis

Summary

The NetAnalysis plugin can be used for analysing a net in regards to certain structural properties like free-choice or marked graph. The plugin also allows to generate a reachability graph. For workflow nets it offers the abilities to check the workflow property and to do a reduction analysis which reduces a workflow net to help determining the soundness.

The plugin was developed in a project and later updated by Michael Haustermann who also implemented the reduction analysis (see Haustermann).

Usage

After starting Renew with the NetAnalysis plugin loaded the new options can be found in Tools->NetAnalysis. With the command “Show Net Representation” a net will be represented as tables and list. The different properties can be checked with “Check Net Graph Properties” which checks all properties at once or with the property specific methods. The reachability graph can be created with the corresponding commands. The command with the addition “graphical” creates a graphical representation as well as a text representation.

The commands for the reduction analysis are “Reduction Analysis” and “Reduction Analysis (with graphical steps)”. For the former the reduction is done in the background and when finished all reducible places and transitions are marked in red. Additionally the console is filled with informations about the used steps and a representation of the reduced net as text. The latter command opens a new window which allows to do the reduction step by step and shows the corresponding reduction rule for each step. Every step is directly applied to the net and can be undone.

The plugins also allows to export a given net to the pep format (Programming Environment Based on Petri Nets (see Grahlmann)).

Examples

The following picture shows the “Check Net Graph Properties” executed on the net mean.rnw which along side other nets is included in the sample folder located in the plugin.

The next picture shows a step of the “reduction analysis (with graphical steps)”

Notes

The reduction analysis is not flawless as there will be for example an exception thrown with the net multifork.rnw which is in the samples folder.

References

Haustermann, Michael (2010). “Analyse von Workflows auf Basis von Petrinetzen”. Bachelorthesis. Vogt-Kölln Str. 30, D-22527 Hamburg: University of Hamburg, Department Informatik.

Grahlmann, Bernd (1997). “The PEP tool”. In: Computer Aided Verification. ed. von Orna Grum- berg. Berlin, Heidelberg: Springer Berlin Heidelberg, S. 440 - 443. isbn: 978-3-540-69195-2.