Formal analysis of BPEL workflows with compensation by model checking

CímFormal analysis of BPEL workflows with compensation by model checking
Közlemény típusaJournal Article
Kiadás éve2008
SzerzőkKovács, Máté, Gönczy, L., and Varró, D.
FolyóiratInternational Journal of Computer Systems and Engineering
Kötet23
Kulcsszavakbusiness process, graph transformation, verification
ÖsszefoglalásIn 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.
URLhttp://www.mit.bme.hu/ varro/publication/2008/ijcsse08-kgv.pdf