Semantic Notions of Weakly Correct AND/XOR Business Workflows Based on Partial Synchronization

Workflows coordinate the execution of multiple tasks or services. This paper presents a novel approach to model workflows based on partial synchronization. We develop new notions of weak correctness called semantic correctness and redundancy soundness that permit semantically correct execution instances with some partially finished paths, and show how to deal with them by the notion of transactional "undo". The properties of partial synchronization using strong and weak corresponding pairs are analyzed, and illustrated with realistic examples. An algorithm called Weak Verify is developed to check a workflow for weak correctness properties. This algorithm makes use of an existing algorithm for strict verification. Our design approach mimics how end users think about workflows in practice, and we contrast it with other notions of strict and weak correctness. We compare our approach with various other approaches.