Research On Formal Modeling Of Message Passing Based On Coloured Petri Nets

The communication rules between nodes are the base of networks on the distributed systems. With the increasing demand of the network services, the complexity of network systems are represented through space distribution, concurrence, asynchronism, instability and diversity in protocols. Systems engineering methods are required to design and maintain the systems during the lifecycle of systems. And the mathematic graphics are also needed to formalize systems, in order to check validity, evaluate performance, realize the design goals and test systems. The message passing is an important communication mode between hosts in distributed systems, so the researches on its realization mechanism get especially necessary. However, in these days many of development methods about distributed message passing still have been not established by aiming specially at the characteristics of distributed system, at the cost of the increase of development costs and risks. Due to the increasing complexity of practical problems, the demand for the formal technologies to solve these problems is growing. This paper, to begin with, studied a distributed message passing based on the combination mode of broadcast request and point-to-point response (MPCBP). The layered CPNs, a formal method, were used to descript the process of sending and receiving messages and the communication between hosts. After Analyzed in detail the fired transitions starting at some initial markings and the correlative replacements, the reachability graph of some sub-pages were built. Moreover, turned to the CPN Tools, this paper checked the dynamic properties of the whole MPCBP system model through the state space generated in automatic manner. The performance analysis conclusion was drawed which relied on the timed CPNs(TCPN) and some calculate methods. The detail discussion and main contribution are listed as follows: (1) This paper provided theoretically the basic architecture of the MPCBP message passing. The feasibilities of utilizing the characteristics which the CPNs can be used to correctly simulate distributed and dynamic behaviors to formally describe and analyze the MPCBP system were also discussed. (2) The MPCBP message passing mechanism was formalized through the formal method which based on the CPNs theory. In the formal system, the hosts send the request packets by the broadcast communication methods, whereas deliver the response messages with the point-to-point mode. And checking loss and retransferring the request packets when the loss of the message packets happened to the system also were researched in this paper. (3) The wormhole routing was realized through this formal method at a certain extent. As a result of this formal realization, the message flits can be transmited orderly in model system, and the dirty messages can be droped and the corresponding request packets can be retransferred. At the same time, the message flits will flow continuously in the system. (4) After a series of formal descriptions, the paper analyzed the state space of the MPCBP model system. The dynamic properties, such as reachability, boundedness, home property, liveness property and fairness property, of the whole MPCBP system model were checked through the state space generated in automatic manner. (5) Through simulating time after time, this paper gained some performance parameters, included the delay time and the network bandwidth, in the case of adopting the different retransmission time intervals. And after analyzed and evaluated these conclusions, the most moderate retransmission time interval was determined.