的个人主页 http://faculty.nuaa.edu.cn/zhouyu/zh_CN/index.htm
点击次数:
所属单位:计算机科学与技术学院/人工智能学院/软件学院
发表刊物:FRONTIERS OF COMPUTER SCIENCE
关键字:distributed computing hierarchical leader election protocol dynamic systems probabilistic model checking
摘要:Leader election protocols are fundamental for coordination problems-such as consensus-in distributed computing. Recently, hierarchical leader election protocols have been proposed for dynamic systems where processes can dynamically join and leave, and no process has global information. However, quantitative analysis of such protocols is generally lacking. In this paper, we present a probabilistic model checking based approach to verify quantitative properties of these protocols. Particularly, we employ the compositional technique in the style of assume-guarantee reasoning such that the sub-protocols for each of the two layers are verified separately and the correctness of the whole protocol is guaranteed by the assume-guarantee rules. Moreover, within this framework we also augment the proposed model with additional features such as rewards. This allows the analysis of time or energy consumption of the protocol. Experiments have been conducted to demonstrate the effectiveness of our approach.
ISSN号:2095-2228
是否译文:否
发表时间:2018-08-01
合写作者:Zhou, Nvqi,Han, Tingting,Gu, Jiayi,Wu, Weigang
通讯作者:周宇