Gesellschaft fr Informatik e.V.

Lecture Notes in Informatics

Business Process, ServicesComputing and Intelligent Service Management P-147, 81-94 (2008).

Gesellschaft für Informatik, Bonn


Witold Abramowicz, Leszek Maciaszek, Ryszard Kowalczyk, Andreas Speck (eds.)

Copyright © Gesellschaft für Informatik, Bonn


Verifying business rules using an SMT solver for BPEL processes

Ganna Monakova , Oliver Kopp , Frank Leymann , Simon Moser and Klaus Schäfers


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: PDF

Gesellschaft für Informatik, Bonn
ISBN 978-3-88579-241-3

Last changed 24.01.2012 22:05:08