On Web Services Transaction Based On Extended π Calculus

With the rapid development of e-business, web applications based on the Web are developed rapidly. Thus, web services technology which is widespread accepted instantiation of service oriented computing has become a effective solution to e-business. Web services technology is considered as the third revolution of IT technology following PC and Internet. Perspective of web services is most accredited in the view of application of e-business. However, some key technologies of web services are not solved well. So there are many interested things to research.Different component web services in the composition have the requirement of consistence and soundness of operations, so need the support of transaction process. In this thesis, we mainly discuss the fomal analysis of web services composition and web services transaction.This thesis firstly presents the concept of web services, its archetecture and characteristic. And then we enumerate some technologies about web services such as XML, SOAP, WSDL, UDDI. For so-called choreography and orchestration language, we not only discuss the difference between them but also point out that they are synergic. We also analyse the characteristics of web services transaction and introduce mechanism of web services transaction such as BTP, WS-C/T, WS-TXM. In order to use π calculus we give its basic syntax and semantics.Basis of above contents, we use the extended π calculus to establish fomal model, and in order to grasp the key concepts the model stems from the existing proposals but is independent of them. We specialise web services composition with extended π calculus. Moreover we character the characteristics of web services transaction with extended real-time π calculus and emphasize its strong(weak)time bisimulation and time granularity based bisim-ulation.The main contributions of this thesis are as following:· Extending π calculus with [P, Q]_t, (?)[P, Q]_t; R(?)_x and signal(t), the syntax and semantics are defined, the laws such as scope laws, transaction laws, floating laws are given. In order to illustrate expressivity of the model a case is studied.· We extend real-time π calculus with sturcture of transaction and define the functor t(α) to express the time of execution of action. For the character of time persistency of real-...