Article in Proceedings INPROC-2009-33

BibliographyMonakova, Ganna; Kopp, Oliver; Leymann, Frank; Moser, Simon; Schäfers, Klaus: Verifying Business Rules Using an SMT Solver for BPEL Processes.
In: Proceedings of the Business Process and Services Computing Conference: BPSC'09.
University of Stuttgart, Faculty of Computer Science, Electrical Engineering, and Information Technology.
Lecture Notes in Informatics, english.
Gesellschaft für Informatik e.V. (GI), March 2009.
ISBN: 978-3-88579-241-3.
Article in Proceedings (Conference Paper).
CR-SchemaH.4.1 (Office Automation)
Keywordsconstraint verification
Abstract

WS-BPEL is the standard for modelling executable business processes. Recently, verification of BPEL processes has been an important topic in the research community. While most of the existing approaches for BPEL process verification merely consider control-flow based analysis, some actually consider data-flows, but only in a very restrictive manner. In this paper, we present a novel approach that combines control-flow analysis and data-flow analysis, producing a logical representation of a process model. This logical representation captures the relations between process variables and execution paths that allow properties to be verified using Satisfiability Modulo Theory (SMT) solvers under constraints represented by the modelled assertions.

Full text and
other links
BPSC 2009
Volltext
Department(s)University of Stuttgart, Institute of Architecture of Application Systems
Project(s)MASTER
Entry dateMarch 19, 2009
   Publ. Institute   Publ. Computer Science