Beyond Soundness: On the Semantic Consistency of Executable Process Models

Executable business process models build on the spec-ification of process activities, their implemented business functions (e.g., Web services) and the control flow between these activities. Before deploying such a model, it is impor-tant to verify control-flow correctness. A process is sound if its control-flow guarantees proper completion and there are no deadlocks. However, a sound control flow is not suf-ficient to ensure that an executable process model indeed behaves as expected. This is due to business functions re-quiring certain preconditions to be fulfilled for execution and having an effect on the process (postconditions). Semantic annotations provide a means for taking such further aspects into account. Inspired by OWL-S and WSMO, we consider process models in which the individual activities are annotated with logical preconditions and post-conditions specified relative to an ontology that axiomatizes the underlying business domain. Verification then means to determine whether the interaction of control flow and log-ical states of the process is correct. To this end, we for-malize the semantics of annotated processes and point out which kinds of flaws may arise. We then identify a class of processes with restricted semantic annotations where cor-rectness can be verified in polynomial time; and we prove that the semantic annotations cannot be generalized with-out losing computational efficiency. The paper is written at a semi-formal level using an illustrative example, details can be looked up in a longer technical report. 1