[1] Gu Xiwu, Li Ruixuan, Lu Zhengding,. Typed formal model for WS-CDL specificationof web services composition [J]. Journal of Southeast University (English Edition), 2008, 24 (3): 300-307. [doi:10.3969/j.issn.1003-7985.2008.03.012]

Copy

Typed formal model for WS-CDL specificationof web services composition()

Share：

Journal of Southeast University (English Edition)[ISSN:1003-7985/CN:32-1325/N]

Volumn:

24

Issue:

2008 3

Page:

300-307

Research Field:

Computer Science and Engineering

Publishing date:

2008-09-30

Info

Title:

Typed formal model for WS-CDL specificationof web services composition

Author(s):

Gu Xiwu;  Li Ruixuan;  Lu Zhengding

College of Computer Science and Technology, Huazhong University of Science and Technology, Wuhan 430074, China

Keywords:

typed model;  web services composition;  web services choreography description language

PACS:

TP311

DOI:

10.3969/j.issn.1003-7985.2008.03.012

Abstract:

In order to formally reason and verify web services composition described by web services choreography specification WS-CDL, a typed formal model named typed abstract WS-CDL(web services choreography description language)for WS-CDL specifications is proposed.In typed abstract WS-CDL, the syntax of type and session, typing rules and operational semantics are formalized;the collaborations of web services are formally described by sessions;the operational semantics of a session can help to formally reason the execution of the choreography;the typing rules can help to formally check the data type consistency of exchanged information between web services and capture run-time errors due to type mismatches.Particularly, the concepts of type assumption set extension and type assumption set compatibility are proposed, and the merging algorithm of type assumption sets is defined so as to eliminate type assumption conflict.Based on the formal model, typed mapping rules for mapping web services choreography to orchestration is also defined.With the typed mapping rules, orchestration stubs and their type assumption sets can be generated from a given choreography; thus, web services composition can be verified at choreography and orchestration levels, respectively.The model is proved to have properties of type safety, and how the model can help to reason and verify web services composition is illustrated through a case study.

References:

[1] Bucchiarone A, Gnesi S.A survey on services composition languages and models [C]//Proc of the International Workshop on Web Services Modeling and Testing.Palermo, Italy, 2006:51-63.
[2] Kavantzas N, Burdett D, Ritzinger G, et al.Web service choreography description language version 1.0[EB/OL].(2005-11-09)[2008-04-01].http://www.w3.org/TR/2005/CR-ws-cdl-10-20051109/.
[3] Salaun G, Bordeaux L, Schaerf M.Describing and reasoning on web services using process algebra [C]//Proc of the 2nd IEEE International Conference on Web Services.Washington, DC:IEEE Computer Society Press, 2004:43-50.
[4] Brogi A, Canal C, Pimentel E, et al.Formalizing web service choreographies [J].Electronic Notes in Theoretical Computer Science, 2004, 105:73-94.
[5] Busi N, Gorrieri R, Guidi C, et al.Towards a formal framework for choreography [C]//Proc of the 14th IEEE International Workshops on Enabling Technologies:Infrastructures for Collaborative Enterprises. Washington, DC:IEEE Computer Society Press, 2005:107-112.
[6] Yeung W L, Wang J, Dong W.Verifying choreographic descriptions of web services based on CSP [C]//Proc of the IEEE Services Computing Workshops(SCW’06).Washington, DC:IEEE Computer Society Press, 2006:97-104.
[7] Zhao Xiangpeng, Yang Hongli, Qiu Zongyan.Towards the formal model and verification of web service choreography description language [C]//Proc of the 3rd International Workshop on Web Service and Formal Methods. Springer-Verlag, 2006:273-287.
[8] Gay S, Hole M.Subtyping for session types in the pi calculus [J].Acta Informatica, 2005, 42(2):192-225.
[9] Pahl C.A pi-calculus based framework for the composition and replacement of components [C]//Proc of Object-Oriented Programming, Systems, Languages, and Applications(OOPSLA’2001)—Workshop on Specification and Verification of Component-Based Systems. New York:ACM Press, 2001:97-107.
[10] Gu Xiwu, Lu Zhengding.A typed formal model for web services composition [J].Computer Science, 2008, 35(1):128-134.
[11] Sangiorgi D, Walker D.The pi-calculus:a theory of mobile process [M].Cambridge:Cambridge University Press, 2001:231-308.
[12] Victor B, Moller F.The mobility workbench—a tool for the pi-calculus [C]//Proc of the 6th International Conference on Computer Aided Verification. Springer-Verlag, 1994:428-440.

Memo

Memo:

Biographies: Gu Xiwu(1967—), male, doctor, lecturer, guxw_wang@sina.com; Li Ruixuan(1974—), male, doctor, associate professor, rxli@hust.edu.cn.
Foundation items: The National Natural Science Foundation of China(No.60403027, 60773191, 70771043), the National High Technology Research and Development Program of China(863 Program)(No.2007AA01Z403).
Citation: Gu Xiwu, Li Ruixuan, Lu Zhengding.Typed formal model for WS-CDL specification of web services composition[J].Journal of Southeast University(English Edition), 2008, 24(3):300-307.

Common functions