Modeling And Analyzing Of Publish/Subscribe Systems Based On Colored Petri Nets Theory

Along with the distributed systems being extensively into use, the distributed systems have changed a lot in application range and scale, which ask communicating models to accommodate to the change of large scale, asynchronism, and multipoint communication. For the fast coupling of distributed systems, the traditional communication models cannot accommodate themselves to the changes. Publish/subscribe (pub/sub) systems adapt to the dynamic and changeable large-scale distributed computing environment demands. Because the technology has some characteristics: asynchronous, loosely-coupled and multi-corresponding and so on. So recent years many people have studied them, but most papers in existing pub/sub systems suffer a number of problems on the expressiveness, efficiency and reliability, which can not satisfy the need of large-scale distributed computing environment demands. For the dispersion control, the fault-tolerant ability as well as self-organization of P2P technology, it will bring to the systems strong fault-tolerant ability and reliability of transmission if publish/subscribe systems are combined with the P2P technology. Many factors must be taken into consideration, which makes the network more complex, especially in space distribution, concurrence, asynchronism, instability and diversity. So systems engineering methods are required to design and maintain the systems during the lifecycle of systems. And we would formalize the system, check validity, and evaluate performance during the lifecycle of designing a system. Therefore it is necessary to carry on the formalize method to design. There are many formal methods to carry out them now. According to the publish/subscribe systems and P2P network, Colored Petri Nets are chosen as my method. The system is modeled in detail for a message from being sent to being received. The CPN model can reflect the dynamic process, make the protocol strong fault-tolerant ability and reliability, and make sure that each subscriber can receive the message once and only once.Before modeling some supposes and promises of the systems are given just for simplicity, but it makes no difference to the dynamic properties of the system. The result can help us analyze reliability of transmission and improve the protocol.This paper introduces Colored Petri Nets theory, pub/sub systems, and the merit when they are combined. Then, describes the router protocol of the pub/sub systems in formal theory, including the disposal of subscribing and publishing. And next gives extended models. Then the CPN models using the CPN Tools are analyzed. The dynamic properties, such as reachability, boundedness, home property, liveness property and fairness property, of the whole system model are checked through the state space generated in automatic manner. These verify the rooting protocol of publish/subscribe systems in favor of comprehensively study the protocol,and prove the usability of the protocol for networks,and also can find the problems in the protocol. This is significant for the improvement and development of the protocol. At last, the result and the next work are given.