Research On BufferPetri Net Semantic Translation For A New-type Pi Calculus

In the past few decades, with the development of computer science and communicationstechnology, interactive systems have become increasingly popular, and the way of computinghas changed a lot from the traditional sequential calculation extended to the concurrentcomputing with interaction as the main feature, simultaneously both location and mobility arecharacterized as independent concepts in the formal model. Pi calculus proposed by RobinMilner is a kind of process algebra method describing concurrent interactive systems, whosebasic entities are processes and names. The syntax and semantics of Pi calculus can be foundin the Reference, and they are not repeated here. Pi calculus is a computational model basedon synchronization interactive pattern with a lack of asynchronous features. However, withthe development of network technology, asynchronous communication technology with Ajaxas the representative has become a mainstream, so it requires a corresponding formal methodto describe and analyze systems with asynchronous features.From the property and application of Pi calculus, Pi calculus is a concurrent calculationmodel which is suitable to describe the dynamic change of topological structure, especiallyloosely coupled systems of node mobility characteristics, such as mobile communicationsystems, and the attribute and behavior of the systems is carrying on analysis by theappropriate mathematical methods. With the characteristics of simplicity and meticulousnesson math, but As Pi calculus is of high abstract, then it isn’t able to accurately simulate all thereal-world behavior patterns, and when Pi calculus is applied to model the systems, theexpression of Pi calculus is too cumbersome and complex, and the real physical structure ofthe modeled systems isn’t reflected, the constraints and norms of behavior in the systemrequirements is lack of the expression ability, the true concurrent behavior of the systems cannot be described, the analytical tools which support the validation of Pi calculus is less, andthere are only several automation validation tools such as MWB and HAL.Compared to Pi calculus, Petri nets are graphical mathematical tools. It has a graphicalrepresentation of simplicity and intuition, and is the mathematical expression as the basis foranalysis and modeling, so Petri net is also a form of strictness, it is very suitable fordescribing the concurrent distributed, asynchronous system, and it is a good description of thephysical structure of the systems and the constraints and norms of behavior in systemrequirements, and the true concurrent behavior can be realistically simulated. Petri net has awide range of automated verification analysis tools, which can meet the needs of industrialand engineering very well. However, in the process of the fomal modeling of the traditional mature systems, the actual difficulties exist when Petri net is used to model the system inpractice, because the systems of the various areas vary widely, each modeling ideas andmethods are not unified, a generalized method can not be summed up, so that the promotion islimited in scope. However for some emerging areas, such as mobile communication field, thegraphic characteristics of Petri net also limit the descriptive power, so that it can not beaccurately expressed.Compared with the two modeling methods, they have their respective advantages. Picalculus has the strong capability of expansion, so firstly, the asynchronous expansion of Picalculus makes the Pi calculus with the characteristics of asynchronous processing, secondlydepending on the unified convenient features of the Pi calculus modeling method, the actualsystems are modeled to apply the extended Pi calculus. At the same time, the general methodof the semantic translation from the extended Pi calculus to Petri net is given here, and thenthe Petri net semantics of specific asynchronous interaction behavior pattern is obtained. Bythe powerful validation tools of the Petri net models, the actual systems are analyzed andverified.The innnovative points of this paper include:(1) Propose a new-type Pi calculus with buffers——Buffer-Pi calculus. In the concept ofbuffers, a new labelled transition system is introduced. The Buffer-Pi-calculus behaviorequivalence relations are defined. A number of propositions and properties of Buffer-PiCalculus are given. Give the analysis for asynchronous processing capacity in the system.(2) Define the new Petri net is BufferPetri, and aimed at the characteristics of Buffer-Picalculus, new places, transitions and arcs are defined.(3) Give the general method of the translation from Buffer-Pi calculus to Petri netsemantics. Prove that BufferPetri after the translation and Buffer-Pi calculus expressions aresemantically equivalent.This paper aims to introduce the asynchronous characteristic to the basic Pi calculus,thus enhancing the descriptive power of Pi calculus, and the related operational semantics ofthe extended Pi calculus and Petri are one-to-one, so the gap is bridged between the variant ofPi calculus and Petri. By the proposed formal conversion method, the better analysis can begained under the unified formal framework.