Model-driven approach supporting formal verification for web service composition protocols

2013 ◽  
Vol 36 (4) ◽  
pp. 1102-1115 ◽  
Author(s):  
C. Dumez ◽  
M. Bakhouya ◽  
J. Gaber ◽  
M. Wack ◽  
P. Lorenz
Keyword(s):  
Formal Verification ◽  
Web Service ◽  
Service Composition ◽  
Web Service Composition ◽  
Model Driven ◽  
Model Driven Approach

scholarly journals Model-driven geospatial web service composition

2014 ◽  
Vol XL-6 ◽  
pp. 7-11
Author(s):  
W. Du ◽  
H. Fan ◽  
J. Li ◽  
H. Wang
Keyword(s):  
Web Service ◽  
Service Composition ◽  
Process Model ◽  
Heterogeneous Data ◽  
Web Service Composition ◽  
Dynamic Binding ◽  
Service Chain ◽  
Model Driven ◽  
Geospatial Web Service

A lot of work has been done on the geospatial service composition to support advanced processing, spatial calculation, and invoking of heterogeneous data. However, the quality of service chain is rarely considered and the process model cannot be reused. A modeldriven way of geospatial web service composition is proposed in this work, the service composition is treated as an optimization problem by <i>GwcsFlow</i> model and dynamic binding mechanism. The case of facility location analysis is provided to demonstrate the improvements in geospatial service composition through optimization algorithms.

A Formal Verification for Web Service Composition Based on CCS

2008 ◽  
Vol 392-394 ◽  
pp. 330-334 ◽  
Author(s):  
B.S. Yun ◽  
J.W. Yan ◽  
M. Liu
Keyword(s):  
Formal Verification ◽  
Web Service ◽  
Service Composition ◽  
Composition Operators ◽  
Web Service Composition ◽  
Composition Algebra ◽  
Dynamic Behaviors ◽  
Formal Tool ◽  
Transformation Mechanisms

Web service composition is a complex and error-prone process. To guarantee its correctness, CCS is exploited as a formal tool to model Web service composition. Composition algebra is defined to specify the rules through which a compositive service can be generated. The transformation mechanisms from service compositions into CCS formalisms according to their corresponding composition operators are gone into details. Then, the automatic reasoner CWB is used to validate the constructed model, by which the dynamic behaviors of the model can be verified and such composition errors as deadlocks can be detected in advance, thus enhancing the composition reliability and avoiding runtime failure. Finally, an example is given to illustrate the effectiveness of this approach.

Sign in / Sign up

Export Citation Format

Share Document