A Formal Verification for Web Service Composition Based on CCS
Bensheng Yun, Jian Yan - - -, Ming Liu · Key engineering materials · 2008
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.