| Mobile communication has entered the third generation mobile communication age, and developing rapidly towards to the fourth generation mobile communication age. With the emergences of new technology, mobile communication service's development trend has been increasing rapidly, these developments will allow mobile users enjoy the mobile communication services that have greater varieties, faster data transmissions, and more powerful functions, including multimedia information, e-commerce, and some other broadband data services. Internet's maturity and IP technology's extensive application make the current 3G mobile communication services are no longer confined to the traditional voice service, and they are trying to merge the traditional mobile network and other broadband network together, thereby, the mobile communication could makes great efforts to realize the multimedia services based on IP.UMTS (Universal Mobile Telecommunications System) is a technology of the third generation brought up by the European 3GPP organization, its core net includes Packet Switched (PS) and Circuit Switched (CS), and brought in the IMS (IP multimedia subsystem), witch is used to control the IP multimedia services. Its continuous developments make the communication network progressing towards the network based on IP, and make more services being put into use.Web Service was developed with computer network, it means services offered by web. Along with the development of computer network, Web Service has a wide range of applications and fast development. In current web economic, Web Service is taken seriously more and more. The cloud computing is a kind of Web Service essentially, witch developed by a lot of famous global company. In the information age, Web Service will play an enormous role in people's life.The Pi-calculus was established and put forward by British famous scientist Robin Miler in 1991, who was a winner of the A.M. Turing Award. Pi-calculus broke the thinking witch thought communication as additional action, and regards the computers and procedures as composed by several parts communicating with each other, it is a new kind of modeling method. The current study of Pi-calculus includes two directions, the expanding of Pi-calculus theoretical aspects and the modeling study of practical problems using Pi-calculus as a modeling tool.Pi-calculus, as a new process algebra language, has a certain amount of research and application in Web Service. Pi-calculus entities and Web Service entity have some relations, so that Pi-calculus can make formal description with Web Service, used to research and validation.This paper combines Web Service, the third generation mobile communication core net and Pi-calculus together to discuss and research the third generation mobile communication's web service applications.The paper chooses two processes of the third generation mobile communication:1.the Authentication process of a roaming mobile user accessing to the IP multimedia subsystem. 2.the typical service offered by the IP multimedia subsystem—Presence service. The first process relates to authority access, it has representativeness in secure interaction, the second one is a typical service of the third generation mobile communication, and it could offer the presence information and be a basic service for other mobile communication services, so it has representitiveness of the services of the IMS net. It is clear that these two different communication processes have their own representativeness and research value in different aspects.Main part of this paper is modeling the above two IP multimedia subsystem related processes, by analyzing the communication processes, defines news forms reasonably, and completes the whole modeling work. After the modeling, the paper summarizes a method to describe Web Service based on Pi-calculus, witch suitable for this paper's models. This method is different from Pi-calculus modeling, it is no longer describes the model by entities as a unit, but by the whole service process as a unit, so we can get a clear description of the service process.At last, this paper uses MWB (Mobility Workbench), the automatic verification tool of Pi-calculus, to verify the two models built in this paper, and proves they are correct in aspects of syntax, semantics, deadlocks and so on. In addition, this paper simulates Presence service which is the more representative in the service aspect of the two models, useing the development tools of Web Service, and realizes its complete functions, thus making further improvement on the research process. |
PDF Full Text Request