-
题名基于概率模型的Raft协议形式化验证
- 1
-
-
作者
管金平
杨晋吉
杨成龙
-
机构
华南师范大学计算机学院
-
出处
《计算机与现代化》
2023年第9期77-81,86,共6页
-
基金
广东省自然科学基金资助项目(2020A1515010445)。
-
文摘
共识协议作为分布式系统的关键要素和核心组件,用于解决分布式场景下可能出现故障的节点间保证同一数据一致的问题,其准确性和高效性直接决定了系统的性能。Raft共识协议是目前分布式系统中常见且有效的算法。本文首先使用概率模型检测方法对Raft共识协议进行形式化建模,然后利用概率模型检测的属性规约技术对它的相关属性进行描述,最后通过模型检测工具验证并分析Raft共识协议的一致性和高效性。实验结果表明,Raft共识协议满足一致性,但是在领导者选举阶段,当跟随者维护的最新日志序号的差值范围增加时,选举回合数也会增多,使得整个服务周期选举时间增加,从而影响协议的执行效率。
-
关键词
分布式系统
raft共识协议
概率模型检测
形式化验证
属性规约
-
Keywords
distributed system
raft consensus protocol
probabilistic model checking
formal verification
property specification
-
分类号
TP391
[自动化与计算机技术—计算机应用技术]
-