Compositional modeling and verification of workflow processes

Abstract

Workflow processes are represented as Petri nets with special entry and exit places and labeled transitions. The transition labels represent actions. We give a semantics for such nets in terms of transition systems. This allows us to describe and verify properties like termination : the guaranteed option to terminate successfully. We describe the composition of complex WF nets from simpler ones by means of certain operators. The simple operators preserve termination, giving correctness by design. Only the advanced communication operators are potentially dangerous. A strategy for verification of other properties is described.