Abstract:Based on the study of traditional publish/subscribe message middleware, we study the publish/subscribe message middleware with the combination of the characteristics of Gossip Protocol. Finally we use the PRISM simulation tools to formally analyze the simulation model with the formal methods. The experimental results show that the real-time performance of the publish/subscribe message middleware system is affected by the message generation rate, and under the two condition of each subscriber subscribe the same messages or different messages, the network characteristics show different changes, but ultimately decreases with the increase of the message generation speed. The reliability decreases with the increase of the message generation speed, and increases with the increase of subscriber's receive buffer, but the increase rate will become increasingly smaller. The experimental model and experimental methods will certainly help for studying the publish/subscribe message middleware system and adjusting the system parameter in the real environment.