Uma - an Unfolding-based Model Analyzer

Uma is a tool for analyzing behavioral properties of Petri nets and scenario-based specifications, and for synthesizing Petri nets from scenario-based specifications.

The theory behind Uma generalizes McMillan's complete prefixes of Petri net unfoldings; see my PhD thesis From Scenarios To Components to learn more.

Uma is implemented in Java and runs as a stand-alone tool; alternatively you may use Uma as an unfolder library in your own tool. Currently, Uma is used as a library in

• Greta
• the Process Mining Toolkit ProM
• BPstruct

go to Github to learn more and download Uma and its source code

Sam - tools for Scenario-based Analysis and Methods

Sam provides tools for analyzing and discovering scenarios and for synthesizing Petri nets from scenario-based specifications.

go to https://www.win.tue.nl/~dfahland/tools/sam/ to learn more and download Sam

Greta - a Graphical Runtime EnvironmenT for Adaptive Processes

Greta is graphical editor and simulation engine for scenario-based specifications in the style of Live Sequence Charts. You can use Greta to

• specify the behavior of a distributed system in scenarios,
• execute your specification in an animated simulation,
• verify behavioral properties of your specification, and
• synthesize Petri net components from a scenario-based specification.

Greta builds on Eclipse and can be installed as a plugin to your running Eclipse installation, or as a stand-alone application.

go to http://home.gna.org/service-tech/greta/ to learn more and download Greta
get the source code of Greta and of the underlying Seda tool

Uma/Prom : Unfolding-based Tools for Process Mining

We use the technique of McMillan's complete prefixes in several plugins for the Process Mining Toolkit ProM. These plugins allow

• Analyze behavioral properties of mined Petri nets,
• Structurally simplify mined Petri nets (while preserving their behavior),
• Repair model based on recorded executions in a log.

go to http://www.processmining.org to learn more and download the Uma plugins for ProM and their source code

UML2oWFN

Uml2owfn is a tool for translating process models created with the IBM Websphere Business Modeler into Petri net models to enable structural and behavioral analysis. The translation implemented in uml2owfn is described in a technical report.

go to http://home.gna.org/service-tech/uml2owfn/ to learn more about UML2oWFN and to download the tool and its source code