Formal semantics and analysis of control flow in WS-BPEL Export

@article{citeulike:1668772, abstract = {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.}, author = {Ouyang, Chun and Verbeek, Eric and van der Aalst, Wil M. and Breutel, Stephan and Dumas, Marlon and Ter}, citeulike-article-id = {1668772}, citeulike-linkout-0 = {http://dx.doi.org/10.1016/j.scico.2007.03.002}, citeulike-linkout-1 = {http://linkinghub.elsevier.com/retrieve/pii/S0167642307000500}, citeulike-linkout-2 = {http://www.sciencedirect.com/science/article/B6V17-4NFR520-1/2/69320d4dd7eeea09793e45cae4866b36}, day = {1}, doi = {10.1016/j.scico.2007.03.002}, journal = {Science of Computer Programming}, keywords = {bpel, ws}, month = {July}, number = {2-3}, pages = {162--198}, posted-at = {2007-09-18 11:32:30}, priority = {2}, title = {Formal semantics and analysis of control flow in WS-BPEL}, url = {http://dx.doi.org/10.1016/j.scico.2007.03.002}, volume = {67}, year = {2007} }

TY - JOUR ID - citeulike:1668772 L3 - citeulike-article-id:1668772 N2 - 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. IS - 2-3 JF - Science of Computer Programming EP - 198 TI - Formal semantics and analysis of control flow in WS-BPEL VL - 67 SP - 162 KW - bpel KW - ws AU - Ouyang, Chun AU - Verbeek, Eric AU - van der Aalst, Wil AU - Breutel, Stephan AU - Dumas, Marlon AU - Ter PY - 2007/07/01/ UR - http://dx.doi.org/10.1016/j.scico.2007.03.002 ER -