Lecture Notes in Computer Science, 2006, Volume 4102/2006, 389-394, DOI: 10.1007/11841760_28

Verifying Workflows with Cancellation Regions and OR-Joins: An Approach Based on Reset Nets and Reachability Analysis

M. T. Wynn, W. M. P. van der Aalst, A. H. M. ter Hofstede and D. Edmond

View Related Documents

Abstract

When dealing with complex business processes (e.g., in the context of a workflow implementation or the configuration of some process-aware information system), it is important but sometimes difficult to determine whether a process contains any errors. The concepts such as cancellation and OR-joins occur naturally in business scenarios but the presence of these features in process models poses new challenges for verification. We take on the challenge of finding new verification techniques for workflows with cancellation regions and OR-joins. The proposed approach relies on reset nets and reachability analysis. We present these techniques in the context of workflow language YAWL that provides direct support for these features. We have extended the graphical editor of YAWL with these diagnostic features.

Keywords  Workflow verification – Cancellation – OR-joins – Reset nets – YAWL

Fulltext Preview

Image of the first page of the fulltext document