Research Of A Formal Model For WS-CDL Based On Trace With Conditions

With the rapid development of the Internet,people paid more attention to the technology of Web service.But,Web service with a single function is no more adequate to enterprise applications. Web service composition is a research about how to make the organic integration of kinds of interrelated web services,and how to form powerful enterprise level services in order to accomplish business goal.Now,there is a whole new method for web service composition called choreography,which is used to describe peer-to-peer collaborations of some participants at a higher level.The specification of choreography is Web Services Choreography Description Language(WS-CDL),which from a global viewpoint describes the composition of some services that are based on interaction,the common and complementary observable behavior,and the jointly agreed ordering rules.But, WS-CDL lacks of formal model,and lacks of the definition of implementation.At present,many research works on formal model of WS-CDL are incomplete in many ways,or don't involve the issues about implementation and conformance.Therefore,to improve the modeling-related work on WS-CDL has great significance.Summarizing and extending the existing modeling methods,we propose a concept called trace with conditions,under which we define a syntax and semantic rule for WS-CDL specification,as known as global model.In order to discuss implementation,we define a syntax and semantic rule for WS-CDL specification in every-single role,as known as local model,and give the mapping process from global model to local model.Then,we rigorously define the implementation,and give an algorithm to implement the choreography between all roles.And we also discuss the conformance problem under the model above.At last,we list the data structure and part of the code to illustrate the algorithm,and demonstrate the validity.