Verifying Workflows with Cancellation Regions and OR-joins: An Approach Based on Relaxed Soundness and Invariants

Abstract

The YAWL (Yet Another Workflow Language) workflow language supports the most frequent control-flow patterns found in the current workflow practice.As a result, most workflow languages can be mapped onto YAWL without loss of control-flow details, even languages allowing for advanced constructs such as cancellation regions and OR-joins.At the moment no analysis techniques are available for such languages, because both cancellation regions and OR-joins are "non-local" properties and therefore difficult to verify.Hence, a verification approach for YAWL is desirable, because such an approach could be used for any workflow language that can be mapped onto YAWL.This paper introduces a verification approach for YAWL that abstracts from the actual semantics of the OR-join.This approach is correct (errors reported are really errors), but not necessarily complete (not every error might get reported).This incompleteness is due to the fact that the approach approximates the OR-join semantics.Nevertheless, our approach can be used to successfully detect errors in YAWL models.Moreover, the approach can easily be transferred to other workflow languages allowing for advanced constructs such as cancellations and OR-joins.

Cite this work

No public copy is stored for this record, so only the metadata is cited.

Stored only when both papers are in the corpus — 70 citations exist upstream.

Papers that cite the same references — the relational fallback while embeddings are still backfilling.