| With the rapid development of Internet techniques, Web Services are becoming more and more popular. Deployed in the internet, Web Service refers to those software components with charicteristics of independence, self-containing, self-description and modularization; also, they are interfaces used to describe some operations. The interfaces hide the details of implementing services, and allow using services independent on software and hardware platform that were used for implementing services and programming language with which implemented service. And applications running over Web Services become loose coupling, component oriented and platform independent. It can perform a specific assignment or a group of assignments. Cooperated with other services, they can implement complex group or business transactions. Web Service is an application program, which supply with outside an API that can be called through Web. We can call the application program interface through Web with the method of programming. Exactly, Web Service is an object that was deployed on Web. Combining existing Web Services into greater granularity web applications is direct goal in research of Web Services. It is an important turning point for the development of Web services to apply PI calculus to Web services.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 focusing 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 describe the changeable communication system structure naturally. 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 that supports its analysis methods.Petri net is the mathematical presentation of discrete parallel system. Petri net was invented by Karl A Petri in 1960. Petri net has both rigorous mathematical formulation and intuitive graphical presentation. With rich methods to describe the system and sound system analysis technology, Petri net has been playing an important role in computer science. At the same time, it is a formal graphical modeling tool with strict mathematical meanings. Therefore, it is suitable for describing asynchronous concurrent models of computer systems. Focusing on the structure description and nature analysis, it can effectively portray the true concurrent semantics of the system. It doesn't mean that PI calculus can't portray the general concurrent behaviors, since it is based on the interleaving semantics, and its concurrency can be reduced as non-deterministic selection, therefore, PI calculus may be able to tell the difference between the deterministic selection and the concurrent selection.In recent years, mobility has emerged as a key feature of many complex real life computing systems. In order to model such a feature, dedicated process algebras have been designed, among which a central role is occupied by the PI calculus. The standard presentations of the PI calculus are mainly based on term rewriting and, as a result, it is quite difficult to translate it into automata-based causality and concurrency exhibited by a system. The main problem is that the standard term rewriting rules change the structure of an expression modeling the system, whereas an automata-based representation retains its structure over possible evolutions, and the changes of the state are represented explicitly as net markings.In this paper, we outline a compositional semantical translation from the PI calculus to high-level Petri nets coping with the fundamental problem. Although, for brevity, we restrict ourselves to the finite fragment of the PI calculus without the match and mismatch constructs, the reslting theory is still rich enough to allow the description of non-trivial systems. This translation method can be divided into the following specific steps:1. First of all, indexed PI calculus is extended from PI calculus; the purpose is to translate PI calculus semantics into the domain of Petri nets on the best way. So one needs to know which channels are presently'known'to the external environment, and which ones are migrating restricted channels. Because of this, the extending is to add a indexing to the transitions. the extending process is very simple, but is extremely important.2. Next, a context-based representation of indexed PI terms is defined, because the original syntactic definition of the PI calculus is ill-suited for the compositional translation. Therefore the intermediate process algebra is defined: the context-based representation. The problem is addressed simply based on the separation of their static features (related to control flow) and dynamic features (related to channel substitution and channel binding).3. It is clear that a target Petri nets is to be defined. Similarly, the classic Petri nets is extended corresponding to the semantics of the PI calculus, called PNET. Specifically, two new places including holder place and the tag-place, and new arc: read arcs are defined in PNET. What's more, the PNET composition operators are defined so that a number of smaller Petri nets can be combined to a large Petri nets.4. Based on preparations mentined above, it is very easy to do the translation from the PI calculus to high-level Petri nets. Next, the result of indexed PI expression's labeled transition system is strongly bisimilar to the labeled transition system of PNET has been proved.5. Finally, since the analysis and verification on PNET is very difficult, mobile communication system is modeled by the PI calculus instead of PNET, and is translated into simple Petri nets, in the end, the analysis and verification on the simple Petri nets have been done.As to the future work, Since the work done here is just a beginning, and in the area of semantic transformation, a lot of work remains to be finished, and roman is not built in a day, the whole work will surely take a long period, and needs more people to participate in the research, and here, what has been done in this paper is to do some preparation for later involvers, and absolutely, the development of PI calculus will be better and faster, finally, breakthroughs will happen someday! The translation method proposed here will be improved and eventually, it can support translating of replication algorithm to PNET. Also, the tools used to analyze and veirify the PNET will be designed and realized. |
PDF Full Text Request