Uma is a tool for exploring the state space of a given Petri net or scenario-based specification. It uses a symbolic representation of the state space which explicitly distinguishes true concurrency of independent actions from alternative choices between conflicting actions. The technique is known as (McMillan) unfoldings. It allows Uma to explore concurrent behavior of a distributed system as is, instead of mimicking concurrent behavior by its interleaving which leads to exponentially large state spaces. Consequently, Uma constructs even for large systems with huge state spaces only small structures that precisely describe the entire system behavior.

The specific feature of Uma compared to similar tools is that Uma also analyzes scenario-based specifications, and may synthesize components from a scenario-based specification.

In the context of service-technology.org, Uma can be used for synthesizing service models from scenario-based choreography models.

Understand Uma

We designed Uma as library which can be called from within any graphical environment by passing Java objects to the library. Uma returns its analysis results as Java objects as well. In addition, we provide a command-line interface to invoke Uma with text files.

The current main features of Uma are to

• construct the unfolding of a given Petri net or scenario-based specification,

• synthesize a Petri net from a scenario-based specification, and to decompose this Petri net into compatible service models.

Our graphical environment for scenario-based specifications Greta uses Uma as a library to execute scenario-based specifications and to synthesize Petri nets.

Get Uma