Complex BPMN diagrams with spaghetti-like structures are hard to read. BPStruct helps to simplify such diagrams. The underlying algorithms transform unstructured programs/service compositions/(business) process models into well-structured ones. A model is well-structured, if for every node with multiple outgoing arcs (a split) there is a corresponding node with multiple incoming arcs (a join), and vice versa, such that the fragment of the model between the split and the join forms a single-entry-single-exit (SESE) component; otherwise the model is unstructured. The transformation preserves concurrency in resulting well-structured models.

The motivations are manifold:

• Well-structured models are easier to layout for visual representation.
• Well-structured models are easier to comprehend by humans.
• Well-structured models tend to have fewer errors than unstructured ones and it is less probable to introduce new errors when modifying them.
• Well-structured process models are better suited for analysis with many existing formal techniques applicable only for structured models.
• Well-structured models are better suited for efficient execution and optimization.

Petri nets are a powerful formal model for describing the behavior of concurrent systems. It is often used as formal foundation for verifying the control flow of process models.The Academic Initiative includes Petri nets as a diagram type and offers various correctness criteria in order to identify well-behaving process models. Step-through simulation gives a hint about the control flow semantics.

A Petri net is "sound" if there are no deadlocks and no unreachable transitions. In workflow nets (having one input place and one output place), the net structure defines the initial and the final marking, which in turn are the basis for applying this classical notion of soundness. Weak soundness and relaxed soundness can also be checked by the tool.The implementation is based on a naive state space exploration.

This is sufficient for examples with a small degree of concurrency. More advanced model checking techniques, such as LoLA (available on service-technology.org), allow for a more efficient verification of large state spaces.

After modeling a BPMN process with activity durations and case frequency, you can export the process model and import it into the BIMP business process simulation tool. This tool allows to simulate complex real-world business processes in large-scale scenarios. The system was designed and implemented by Marlon Dumas and colleagues at the University of Tartu. The bimp-simulator is a Google code project.