Formal semantics and analysis of control flow in WS-BPEL

C. Ouyang, H.M.W. Verbeek, W.M.P. Aalst, van der, S. Breutel, M. Dumas, A.H.M. Hofstede, ter

Onderzoeksoutput: Bijdrage aan tijdschriftTijdschriftartikelAcademicpeer review

239 Citaten (Scopus)
1 Downloads (Pure)

Samenvatting

Web service composition refers to the creation of new (Web) services by combining functionalities provided by existing ones. A number of domain-specific languages for service composition have been proposed, with consensus being formed around a process-oriented language known as WS-BPEL (or BPEL). The kernel of BPEL consists of simple communication primitives that may be combined using control-flow constructs expressing sequence, branching, parallelism, synchronization, etc. We present a comprehensive and rigorously defined mapping of BPEL constructs onto Petri net structures, and use this for the analysis of various dynamic properties related to unreachable activities, conflicting messages, garbage collection, conformance checking, and deadlocks and lifelocks in interaction processes. We use a mapping onto Petri nets because this allows us to use existing theoretical results and analysis tools. Unlike approaches based on finite state machines, we do not need to construct the state space, and can use structural analysis (e.g., transition invariants) instead. We have implemented a tool that translates BPEL processes into Petri nets and then applies Petri-net-based analysis techniques. This tool has been tested on different examples, and has been used to answer a variety of questions.
Originele taal-2Engels
Pagina's (van-tot)162-198
TijdschriftScience of Computer Programming
Volume67
Nummer van het tijdschrift2-3
DOI's
StatusGepubliceerd - 2007

Vingerafdruk

Duik in de onderzoeksthema's van 'Formal semantics and analysis of control flow in WS-BPEL'. Samen vormen ze een unieke vingerafdruk.

Citeer dit