Font Size: a A A

Conversion And Verification Of PI Calculus With Compositional Petri Net

Posted on:2011-04-05Degree:MasterType:Thesis
Country:ChinaCandidate:F GaoFull Text:PDF
GTID:2178360305954839Subject:Computer application technology
Abstract/Summary:PDF Full Text Request
In recent years, with the rapid development of Internet techniques, Web services are applied more and more widely . However, because of the limit capability of an individual Web service, it can't meet the real requirement . Composing existing Web services together and forming new , offering more functions Web services can realize the full potential capability,and it is the theory of Web services composition.Now , there are many research methods applied to Web services composition , and PI calculus is an important one of them . Turing award gainer, Robin Milner came up with it , and it's a calculus model used for describing and analyzing concurrent system , which uses inducing in the calculus to presenting the dynamic transforming among processes . In PI calculus , the simplest entity is name , and name can be transferred along channels between processes . A transferred name can be a channel name , so PI calculus can express loose dynamic coupled system , such as mobile system.Compared with PI calculus , Petri net ,which was came up earlier, is a hotspot used in Web services research . Petri net is invented by Karl A Petri , and it's a wonderful calculus model in describing discrete , distributed system which is advantaged in describing asynchronous , concurrent computer system.Comparing the two of them, PI calculus has high expandability , but its expression is not intuitive and it is lack of current supporting software; though Petri net has the graphic character , it is lack of expandability . Therefore finding a translating method between them and uncover their advantages is very useful. Raymond Devillers with others have came up a common method to do this , but they haven't came up a system method to translating recursive terms in PI calculus . So proposing a method in translating recursive terms in PI calculus is the key of this paper.This paper first discusses which PI calculus expressions are recursive structures . In this paper , starting with the expression of the Flood method , we confirm the typical recursive expression . Based on this , by analogy to the recursive structure of programming language , the paper analyzes and solves several issues in translating which must be resolved . The first is how to record the level of each recursive operation . The method proposed by Raymond and others has a very good trail token, which can indicate the level where the current operating is , if modified properly . The second is choice and judgment of certain values . Recursive structure has a character of "real-time - confirmed" , and therefore its choice is different from the result of the common method . For solving this problem , the paper designs specifical net structure to complete the task . The third is the preserving and returning of information . In order to save time and space spending , the first is screening out the information needed to preserve , and then define specific elements of Petri nets to complete the correct preserving and returning of information.Based on this , this paper gives the definition of result network-- rp ' net , and gives the whole translating methods and firing rules of transitions . The method has a model-based feature . Using the translating method , you can efficiently and easily achieve the recursive structure conversion.Followed by a discussion of other forms of PI calculus recursive structure . By analyzing each step of the operation of the former operation and follow-up operation, we give analysis process and conversion results of each recursive structure of PI calculus which can be translated , and instructions for which can not be translated. In the actual research and applicating of complex recursive structure, by analyzing the operation's former operation and following operation to study the expression of the translation , it is a very useful analysis method.At the end , we realize the result net of the typical recursive terms of PI calculus in CPNtools---a simulation tool . Because the tool has no directly support for the new elements of the rp 'net including new tokens, places and arcs , this paper insteads them with corresponding equivalent sub-nets , and realizes it in the tool with some adaptive modification . And we let the result net work in the tool , by validating sequence and result of every step , demonstrating the feasibility and accuracy of the translation methods from the view of experiment.In summary , the translating method proposed in this paper is a model method . In applications , users can use the "former operation - following operation" analysis way , and design the correct translation network based on the certain expression . At the same time , the verification process provided by this paper , it is an example using the current experimental conditions to directly realize and verification . So users can use the same or a similar approach to directly validate the results of their own , and it is convenient and efficient.In the course of the study , this paper found the "unconfirmed" recursive structure in the expression of the PI calculus , and the translation of this more complex forms of expression , will be the next objective of the study . Meanwhile , the focus of this paper is the translating mothed of direct recursive structure in the PI calculus , and the study of more complex indirect recursive translation will be the future direction of work.
Keywords/Search Tags:Web services composition, PI calculation, Petri net, translation of recursive structure, unconfirmed
PDF Full Text Request
Related items