Formal verification for Web service composition: A model-checking approach

2015 ◽  
Author(s):  
Majdi Ghannoudi ◽  
Walid Chainbi
Keyword(s):  
Model Checking ◽  
Formal Verification ◽  
Web Service ◽  
Service Composition ◽  
Web Service Composition

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