Formal analysis of BPEL workflows with compensation by model checking

Máté Kovács, D. Varró, László Gönczy

Research output: Contribution to journalArticle

13 Citations (Scopus)

Abstract

In the paper, we present an approach for the verification of business workflows - captured by BPEL processes - with full support for compensation and fault handling. BPEL processes are transformed into the SAL language to carry out (i) verification of safety and reachability properties and (ii) fault modeling by using the SAL symbolic model checker. Compared to existing solutions for model checking BPEL processes, the main added value of the paper is that (i) potential error propagation paths can also be assessed in addition to traditional verification tasks, and (ii) our approach scales up to relatively large workflows thanks to abstraction techniques and the use of the advanced SAL model checker.

Original languageEnglish
Pages (from-to)349-363
Number of pages15
JournalComputer Systems Science and Engineering
Volume23
Issue number5
Publication statusPublished - Sep 2008

Fingerprint

Formal Analysis
Model checking
Model Checking
Work Flow
Fault
Error Propagation
Scale-up
Reachability
Safety
Path
Modeling
Model
Compensation and Redress
Industry

Keywords

  • Business process
  • Graph transformation
  • Verification

ASJC Scopus subject areas

  • Computer Science(all)
  • Control and Systems Engineering
  • Theoretical Computer Science

Cite this

Formal analysis of BPEL workflows with compensation by model checking. / Kovács, Máté; Varró, D.; Gönczy, László.

In: Computer Systems Science and Engineering, Vol. 23, No. 5, 09.2008, p. 349-363.

Research output: Contribution to journalArticle

Kovács, Máté ; Varró, D. ; Gönczy, László. / Formal analysis of BPEL workflows with compensation by model checking. In: Computer Systems Science and Engineering. 2008 ; Vol. 23, No. 5. pp. 349-363.
@article{e163e704ff5b4b70b0a26fbc98e9cc9f,
title = "Formal analysis of BPEL workflows with compensation by model checking",
abstract = "In the paper, we present an approach for the verification of business workflows - captured by BPEL processes - with full support for compensation and fault handling. BPEL processes are transformed into the SAL language to carry out (i) verification of safety and reachability properties and (ii) fault modeling by using the SAL symbolic model checker. Compared to existing solutions for model checking BPEL processes, the main added value of the paper is that (i) potential error propagation paths can also be assessed in addition to traditional verification tasks, and (ii) our approach scales up to relatively large workflows thanks to abstraction techniques and the use of the advanced SAL model checker.",
keywords = "Business process, Graph transformation, Verification",
author = "M{\'a}t{\'e} Kov{\'a}cs and D. Varr{\'o} and L{\'a}szl{\'o} G{\"o}nczy",
year = "2008",
month = "9",
language = "English",
volume = "23",
pages = "349--363",
journal = "Computer Systems Science and Engineering",
issn = "0267-6192",
publisher = "CRL Publishing",
number = "5",

}

TY - JOUR

T1 - Formal analysis of BPEL workflows with compensation by model checking

AU - Kovács, Máté

AU - Varró, D.

AU - Gönczy, László

PY - 2008/9

Y1 - 2008/9

N2 - In the paper, we present an approach for the verification of business workflows - captured by BPEL processes - with full support for compensation and fault handling. BPEL processes are transformed into the SAL language to carry out (i) verification of safety and reachability properties and (ii) fault modeling by using the SAL symbolic model checker. Compared to existing solutions for model checking BPEL processes, the main added value of the paper is that (i) potential error propagation paths can also be assessed in addition to traditional verification tasks, and (ii) our approach scales up to relatively large workflows thanks to abstraction techniques and the use of the advanced SAL model checker.

AB - In the paper, we present an approach for the verification of business workflows - captured by BPEL processes - with full support for compensation and fault handling. BPEL processes are transformed into the SAL language to carry out (i) verification of safety and reachability properties and (ii) fault modeling by using the SAL symbolic model checker. Compared to existing solutions for model checking BPEL processes, the main added value of the paper is that (i) potential error propagation paths can also be assessed in addition to traditional verification tasks, and (ii) our approach scales up to relatively large workflows thanks to abstraction techniques and the use of the advanced SAL model checker.

KW - Business process

KW - Graph transformation

KW - Verification

UR - http://www.scopus.com/inward/record.url?scp=64549111412&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=64549111412&partnerID=8YFLogxK

M3 - Article

VL - 23

SP - 349

EP - 363

JO - Computer Systems Science and Engineering

JF - Computer Systems Science and Engineering

SN - 0267-6192

IS - 5

ER -