Uma: an Unfolding-based Model Analyzer

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, 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 Uma is free software and is licensed under the GNU Affero General Public License. Other licenses can be negotiated with the author.

The latest source code is available at our SVN repository at svn:// and needs JDK 1.5 (or later) and Apache Ant to compile.

More information for compiling and running Uma from the command-line will be provided soon. In the meantime, Uma can be used from within Greta.