Konferenzbeitrag
Verifying business rules using an SMT solver for BPEL processes
Volltext URI
Dokumententyp
Text/Conference Paper
Zusatzinformation
Datum
2009
Zeitschriftentitel
ISSN der Zeitschrift
Bandtitel
Verlag
Gesellschaft für Informatik e.V.
Zusammenfassung
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.