@InProceedings{efts-2007-kgv,
  author = {M{\\'a}t{\\'e} Kov{\\'a}cs and L{\\'a}szl{\\'o} G{\\"o}nczy and D{\\'a}niel Varr{\\'o}},
  title = {Formal Modeling of BPEL Workflows Including Fault and Compensation Handling},
   booktitle = {EFTS \'07: Proceedings of the 2007 workshop on Engineering fault tolerant systems},
year = {2007},
isbn = {978-1-59593-725-4},
pages = {1},
location = {Dubrovnik, Croatia},
url = {http://doi.acm.org/10.1145/1316550.1316551},
publisher = {ACM},
address = {New York, NY, USA},
abstract = {
Electronically executed business processes are frequently implemented using the
Business Process Execution Language (BPEL). These workflows may be in control of
crucial business processes of an organization, in the same time existing model checking
approaches are still immature i.e. they either seem to loose to much information during
the generation of the analysis model, or the state space explosion prevents from model
checking. We present a formal modeling technique for BPEL workflows including fault and
compensation handling providing exact semantics with a state space size that allows for
model checking. Additionally, error propagation among variables is supported so the
effect of a faulty activity on the entire process can be examined. }
}