用PTA模型形式化分析基于Gossip协议的发布/订阅系统  

Formal Analysis of Gossip Protocol-based Publish/subscribe Systems Using the PTA Model

作　　者：沈思铭[1] 

机构地区：[1]同济大学计算机科学与技术系,上海201804

出　　处：《计算机系统应用》2012年第12期60-66,共7页Computer Systems & Applications

摘　　要：在研究传统的发布/订阅消息中间件系统的基础之上,结合Gossip协议的特点来研究发布/订阅消息中间件,最后运用形式化方法,通过PRISM仿真工具,对仿真的模型进行形式化分析.实验结果表明,发布/订阅消息中间件系统的实时性受消息产生速度的影响,在各个订阅者订阅相同消息和不同消息两种情况之下网络特性展现不同的变化,但最终都是随着消息产生速度的增加而减小.可靠性随着消息产生速度的增加而减小,并且订阅者的接收缓存越大可靠性越高,但增幅率会越来越小.该实验模型和实验方法对于发布/订阅消息中间件系统的研究,以及在现实环境中配置系统的相关参数有一定的帮助.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.

关 键 词：发布 订阅 概率时间自动机(PTA) GOSSIP协议 形式化分析 PRISM 

分 类 号：TP301.1[自动化与计算机技术—计算机系统结构] TP393.04[自动化与计算机技术—计算机科学与技术]