Beyond Soundness: On the Verification of Semantic Business Process Models

Ingo Weber 1 Joerg Hoffmann 2 Jan Mendling 3
2 MAIA - Autonomous intelligent machine
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : The verification of control-flow soundness is well understood as an important step before deploying business process models. However, the control flow does not capture what the process activities actually do when they are executed. Semantic annotations offer the opportunity to take this into account. Inspired by semantic Web service approaches such as OWL-S and WSMO, we consider process models 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 actions and change literature. We introduce a formal execution semantics for annotated business processes. We point out four verification tasks that arise, concerning precondition/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 logic underlying the ontology axioms. For reachability and executability, we identify a class of processes that can be verified in polynomial time by a fixpoint algorithm which we design for that purpose. We show that this class of processes is maximal in the sense that, when generalizing it in any of the most relevant directions, the validation tasks become computationally hard.
Type de document :
Article dans une revue
Distributed and Parallel Database (Weston, Conn.)s, 2010, 27 (3), pp.271-343. 〈10.1007/s10619-010-7060-9〉
Liste complète des métadonnées
Contributeur : Joerg Hoffmann <>
Soumis le : mercredi 10 novembre 2010 - 09:30:06
Dernière modification le : lundi 15 janvier 2018 - 12:20:02
Document(s) archivé(s) le : vendredi 11 février 2011 - 02:27:30


Fichiers produits par l'(les) auteur(s)




Ingo Weber, Joerg Hoffmann, Jan Mendling. Beyond Soundness: On the Verification of Semantic Business Process Models. Distributed and Parallel Database (Weston, Conn.)s, 2010, 27 (3), pp.271-343. 〈10.1007/s10619-010-7060-9〉. 〈inria-00491102〉



Consultations de la notice


Téléchargements de fichiers