Eindhoven University of Technology
The correctness of Business Process Models is of paramount importance for the application on an enterprise level. A severe problem is that several languages for Business Process Modeling do not have formal execution semantics which is a prerequisite to check correctness criteria. In this paper, soundness defines a minimum correctness criterion that a process model should fulfill. In this paper, the authors present a novel approach to reason about soundness based on so-called causal footprints. A causal footprint represents a set of conditions on the order of activities that holds for every case of a process model. They identify three kinds of error patterns that affect the soundness of a process model, namely the deadlock pattern, the multiple termination pattern and the trap pattern.