Workflows as UML Activity Diagrams: Analytical Methods for Control-Flow Verification

Abstract

A workflow is a directed graph that depicts a business process. It consists of tasks linked together by AND and XOR connectors, and is usually drawn as a Petri Net or a UML Activity Diagram; the latter notation has gained in popularity in recent years. Workflows sometimes suffer from behavioral defects such as deadlock, lack of synchronization, and interminable looping. Here we present new analytical results useful for verifying the control flow in workflows represented as UML Activity Diagrams. We make use of the notion of corresponding pair and focus on loop-free structures, allowing connectors to form non-nested and overlapping patterns. The analysis can be extended to workflows with loops. To clarify the significance of our results, we provide illustrations of theoretical and practical interest.