|
Research Prototypes
Restructuring BPMN diagrams using BPStruct
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.
by Artem Polyvyanyy, Luciano García-Bañuelos, Dirk Fahland, Mathias Weske, Marlon Dumas
|
Information Flyer (PDF):
|
|
The motivations for well-structured process models 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.
|
Consequently, some process modeling languages urge for structured modeling. However, one needs to be aware of the limitations that the well-structured process modeling implies: There exist concurrent processes that cannot be formalized as well-structured process models.
|
|
|
Modeling and analyzing place/transition nets (Petri nets)
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.
|
|
|
|
