Paper Info
Title
Rigorous Analysis of Service Composability by Embedding WS-BPEL into the BIP Component Framework
Abstract
Behavioral correctness of service compositions refers to the absence of service interaction flaws, so that essential service properties like deadlock freedom are preserved and correctness properties related to safety and liveness are assured. Model checking is a widespread technique and it is based on extracting an abstract model representation of the program defining a service orchestration or choreography. During model extraction, the original structure of the service composition cannot be preserved and backwards traceability of the verification findings is not possible. We propose a rigorous analysis within the BIP component framework. Being rigorous means that the analyst is able to reason on which properties hold and why. The BIP language offers a sound execution semantics for a minimal set of primitives and constructs for modeling and composing layered components. We formally define the WS-BPEL 2.0 execution semantics and we provide a structure-preserving translation (embedding) of WS-BPEL to BIP. Structure preservation is feasible, due to the formally grounded expressiveness properties of BIP. As a proof of concept, we apply the developed embedding to a sample BPEL program and present the analysis results for a safety property. By exploiting the BIP model structure we interpret the analysis findings in terms of the service interactions stated in the BPEL source code. A significant benefit of BIP is that it applies compositional reasoning on the model structure to guarantee essential correctness properties and avoid, as much as possible, the scalability limitations of conventional model checking.
Year
DOI
Venue
2012
10.1109/ICWS.2012.63
ICWS
Keywords
Field
DocType
model extraction,model structure,conventional model checking,bip component framework,essential service property,bip model structure,abstract model representation,service composition,embedding ws-bpel,service composability,bip language,model checking,rigorous analysis,service oriented computing,semantics,web services,soc,service oriented architecture,correlation,synchronization
Model checking,Programming language,Computer science,Correctness,Deadlock,Business Process Execution Language,Web service,Composability,Orchestration (computing),Database,Liveness
Conference
Citations 
PageRank 
References 
7
0.58
9
Authors
3
Name
Order
Citations
PageRank
Emmanouela Stachtiari1354.66
Anakreon Mentis2172.31
Panagiotis Katsaros326230.51