Distrib Parallel Databases DOI 10.1007/s10619-010-7060-9 Beyond soundness: on the verification of semantic business process models

Abstract The verification of control-flow soundness is well understood as an impor-tant step before deploying business process models. However, the control flow does not capture what the process activities actually do when they are executed. Seman-tic annotations offer the opportunity to take this into account. Inspired by semantic Web service approaches such as OWL-S and WSMO, we consider process mod-els in which the individual activities are annotated with logical preconditions and effects, specified relative to an ontology that axiomatizes the underlying business domain. Verification then addresses the overall process behavior, arising from the interaction between control-flow and behavior of individual activities. To this end, we combine notions from the workflow community with notions from the AI ac-tions and change literature. We introduce a formal execution semantics for annotated business processes. We point out four verification tasks that arise, concerning pre-condition/effect conflicts, reachability, and executability. We examine the borderline between classes of processes that can, or cannot, be verified in polynomial time. For precondition/effect conflicts, we show that the borderline is the same as that of the Communicated by Asuman Dogac. The major part of this work was conducted while the first and second authors worked for SA