| With the rapid development of Internet techniques, Web Services are becoming more and more widely used. Web Services are interfaces of describing some operations. The interfaces hide the details of implementing services, and allow using services independent on software and hardware platform that was used for implementing services and programming language with which implemented service. Permit and support that the application program that is based on Web Services becomes loose couple, oriented component, cross-platform technology implement. Web Service implements some a special assignment or a group of assignment. Web Service can implement complex group or business transaction, alone or with other Web Services. Web Service is an application program, which can expose outside an API that can invoke through Web. We can invoke the application program through Web with the method of programming. Exactly, Web Service is an object that was deployed on Web.Web Service is a way of providing enterprise application through Internet and SOAP, and there is strong portability and interoperability. It is deployed in the internet, which is independent, self-contained, self-described, modular software component. It can be published, found, and called. Combining Web Services that had existed into greater granularity web applications is direct goal in Web Service research.Web Service is convenient to application program integration, but the function of single service is limited, and it can't satisfy the actual requirement. We have to composite the services that existed into new service to supply more and more functions, so that Web Service can actually play potential. With the abroad application of Web Services, Web Service composition technology has triggered a considerable number of research efforts both in academia and in industry. Web Service composition has become an important research subject.Web Service composition means that through service search and interface integration composite some autonomic Web Services according to the requirement, in order to supply new and powerful Web Service. In other word, it is a kind of technology that chooses rather simple and useful Web Services in the internet, then composites them into new service.Nowadays, there are too many disadvantages among the methods of Web Service description, such as lacking for powerful theory support, can't verify the correctness and so on. This paper researches the theory of PI-calculus, and discovers that modeling Web Services with PI-calculus can avoid the disadvantage that list above, and it owns the own special advantage. In the paper, we model Web Service with PI-calculus, and then verify the correctness.PI-calculus arose from 1991, Turing award gainer, England Edinburgh University, Robin Milner came up with it referring to grand union theory in physics, and it is the concurrency theory focus on mobile communication among processes. It is a kind of simple but powerful expressive language. At first, it was designed as a kind of calculus that is used for describing communication system, and it can naturally describe the changeable communication system structure. PI-calculus is a kind of calculus model that is used for describing and analyzing concurrency system, with powerful description ability, and it can represent the intermittent interaction between processes by dynamic evolution structure, and there is strong theory supporting its analysis methods.PI-calculus is a kind of mobile calculus model that is based on mobile concurrency calculus model, such as CCS. It developed CCS, and basic calculus entities are name and process. Communication between processes is completed by passing name. Name is the basic concept of PI-calculus, and value, variable and channel are referred by names. The channel of the PI-calculus owns certain scope, and processes outside the scope can't access for the channel, which makes sure the security of channel communication.Since PI-calculus can pass the variable and value in CCS, and it also can pass channel name, at the same time all of the entities above named"name", don't differentiate them, either, so PI-calculus is able to set up new channel, so that PI-calculus can describe the concurrency system whose structure is changeable all the time. PI-calculus is a kind of process algebra that is based on name. Because name can be transferred in process calculus, so it is named process calculus. Because projection is a kind of algebra calculus, PI-calculus is easy for programming.The paper is based on flow, and PI-calculus as Web Service modeling language. It can express the semantic of Web Service and describe Web Service composition. Why shall we choose PI-calculus as Web Service description language? There are many analogies among PI-calculus'and Web Service's key concepts, at the same time, PI-calculus that is mainly used to describe mobile process, owns certain ascendance when it describes the problem in which composite objects and environment are changeable and complex.Web Services'and Web Service composition's development and application is the main research direction of next generation internet. PI-calculus being used for Web Service is good for the development of Web Service.There are too many problems in mobile communication system now, so the paper proposes that we should improve mobile communication service with the thought of Web Service. Mainly Internet as a developing platform, and encapsulate many Web Service with communication process, and describe these Web Services and Web Services composition by PI-calculus, so implementing every communication process by invoking Web Service or Web Service composition. Give out four examples, in order to explain how to model Web Service by PI-calculus in mobile communication process. They are: modeling mobile communication initialization connection process, modeling mobile communication process, modeling mobile communication base station switching process, modeling recalling process. Describe Web Service composition by PI-calculus, and discuss how to describe dynamic changeable service, and abstract concrete PI-calculus expression.In the research of mobile process calculus, process equivalence is a core problem all the time: it means when two process expression with different syntax formations are behavior equivalence. In process calculus, popular equivalence relation as follow: bisimulation equivalence, test equivalence, trace equivalence and so on, and bisimulation equivalence is most influential of all. The paper summarizes some definitions about PI-calculus bisimulation, and it is the rationale of MWB tool working. If we understand the knowledge about bisimulation, we can use MWB tool for verifying the models with high efficient.MWB is the first automatic verification tool that was developed for PI-calculus, and it can be used for analyzing and verifying the concurrency system, which was described by multi-PI-calculus, CCS and so on. At first MWB was developed in Uppsala University in Sweden, and it can be used under Windows, Linux and so on. MWB is open-source. The paper uses MWB tool for verifying the PI-calculus model to make sure the correctness.MWB tool can discover some basic faults of process definitions when it analyzes the syntax of algebra expression, such as type fault, lacking for synchronism, broken behavior and so on. At the same time we can use the reasoning function of the tool to preclude some common fault. Deadlocks command can check whether deadlock exists, and step command can check process behavior. The paper models mobile communication service by PI-calculus, and analyzes the syntax of PI-calculus expression in the model by MWB tool, and verifies the correctness of process definition, included type fault, lacking for synchronism, broken behavior, deadlock and so on, at the same time the reasoning function of the tool to preclude some common fault. |
PDF Full Text Request