SDN多控制器环境下对Raft一致性算法的改进及正确性证明
发布时间：2020-12-24 18:59
随着软件定义网络（software-defined network,简称SDN）规模的扩大和上层应用的复杂化,单个控制器已经不能满足网络要求,成为网络性能的瓶颈。多控制器集群管理SDN有很多优势,但实现多控制器架构需要解决的最基本问题是多控制器之间保持一致性。在集群中运行Raft一致性算法可以解决一致性问题,但集群中Leader被重新选举时会导致集群不可用。因此本文从集群的可用性出发,为Raft算法增加领导权转移功能,避免因Leader被要求关闭、移出集群等情形导致的集群不可用。本文主要研究内容有:第一,对Raft算法选举部分可以转移领导权的情形进行详细分类,给出选择目标节点的度量与方法。针对多控制器集群的工作特点,选取合适的指标选择目标控制器。第二,使用TLA+语言对领导权转移功能进行形式化描述,并使用TLC工具对增加领导权转移的Raft算法的形式化描述进行检测与验证,从而证明其正确性。第三,讨论多控制器集群中Raft算法的运行环境,使用TLA+语言描述并使用TLC工具对规约进行检测与验证。第四,分析了OpenDaylight（ODL）代码中的Raft算法源码的领导权转移部分,并对选...
【文章来源】：内蒙古大学内蒙古自治区 211工程院校
【文章页数】：69 页
【学位级别】：硕士
【部分图文】：
选举算法规约检测模型
图 4.2 选举算法规约检测结果Figure 4.2 The checking results for election algorithm specification4.4 Raft 算法中 Leader 领导权转移的行为描述.4.1 状态转换行为和消息处理行为由 3.3.3 节可知，由于 Raft 算法的选举部分有选举限制条件，因此 Raft 算法中领导权的具体步骤与将选举算法中领导权转移的具体步骤不同，导致形式化描述也不相同。将权转移的形式化描述加入 Raft 算法时与加入选举算法时有下述几点不同。第一是发生领转移时集群需要停止接收交换机的请求，除了加入 Receiverequest(i, v)行为外，Raft 算法化描述中原有的行为 ClientRequest(i, v)行为将增加一个发生的条件，表示可以放入 Lea志中的请求属于控制器中存储的交换机请求队列，即加入语句 v∈RequestQueue。第二点
SDN 多控制器环境下对 Raft 一致性算法的改进及正确性证明4.5 Raft 算法的 TLC 检测和验证增加领导权转移的 Raft 算法进行形式化描述后，使用模型检测工具 TLC 对上述。首先创建一个 Model，命名为 Model_1，然后给常量赋值。常量 Server 代表合，赋值为集合{1,2,3,4,5}；常量 LoadMin 与 LoadMax 赋值常数 10 和 20；常集合{1..10}；其他常量均赋值为 TLC 工具自带的 Model Value。检测初始状态步关系 Next，并检测规约是否会死锁，如图 4.3 所示。模型检测结果如图 4.4 所表明，模型检测器一直运行，检测执行及关闭时没有抛出异常，说明规约没有
【参考文献】：
期刊论文
[1]一种软件定义网络中的控制器热备份及选举算法[J]. 王文博,汪斌强,陈飞宇,王志明,宫阳阳. 电子学报. 2016(04)
[2]基于行为时序逻辑TLA的Pastry协议的规约与验证[J]. 刘照洋,龙士工. 贵州大学学报(自然科学版). 2015(06)
[3]SDN和NFV对网络变革发展影响综述[J]. 张志强. 现代电信科技. 2015(01)
[4]SDN控制器的调研和量化分析[J]. 江国龙,付斌章,陈明宇,张立新. 计算机科学与探索. 2014(06)
[5]基于TLA+的AFDX冗余管理算法的改进[J]. 库恒,龙士工,罗昊. 计算机工程与设计. 2013(03)
[6]基于TLA的ARQ协议描述与验证[J]. 吴勇,李祥. 计算机安全. 2012(08)
[7]分布式超级节点选举算法[J]. 杜丽娟,余镇危. 计算机工程与应用. 2011(14)
[8]ARP协议的描述与TLA验证[J]. 李元,吴勇,李祥. 计算机技术与发展. 2010(06)
[9]基于TLA+的BRP协议规约及验证[J]. 陈立前,王戟,陈火旺. 计算机工程与科学. 2006(01)
硕士论文
[1]PAXOS算法改进及应用研究[D]. 刘春涨.广西民族大学 2016
[2]基于Zookeeper的SDN多控制器架构的研究与实现[D]. 田心宁.兰州大学 2016
[3]基于行为时序逻辑TLA的网络协议的描述与验证[D]. 刘照洋.贵州大学 2015
本文编号：2936149
【文章来源】：内蒙古大学内蒙古自治区 211工程院校
【文章页数】：69 页
【学位级别】：硕士
【部分图文】：
选举算法规约检测模型
图 4.2 选举算法规约检测结果Figure 4.2 The checking results for election algorithm specification4.4 Raft 算法中 Leader 领导权转移的行为描述.4.1 状态转换行为和消息处理行为由 3.3.3 节可知，由于 Raft 算法的选举部分有选举限制条件，因此 Raft 算法中领导权的具体步骤与将选举算法中领导权转移的具体步骤不同，导致形式化描述也不相同。将权转移的形式化描述加入 Raft 算法时与加入选举算法时有下述几点不同。第一是发生领转移时集群需要停止接收交换机的请求，除了加入 Receiverequest(i, v)行为外，Raft 算法化描述中原有的行为 ClientRequest(i, v)行为将增加一个发生的条件，表示可以放入 Lea志中的请求属于控制器中存储的交换机请求队列，即加入语句 v∈RequestQueue。第二点
SDN 多控制器环境下对 Raft 一致性算法的改进及正确性证明4.5 Raft 算法的 TLC 检测和验证增加领导权转移的 Raft 算法进行形式化描述后，使用模型检测工具 TLC 对上述。首先创建一个 Model，命名为 Model_1，然后给常量赋值。常量 Server 代表合，赋值为集合{1,2,3,4,5}；常量 LoadMin 与 LoadMax 赋值常数 10 和 20；常集合{1..10}；其他常量均赋值为 TLC 工具自带的 Model Value。检测初始状态步关系 Next，并检测规约是否会死锁，如图 4.3 所示。模型检测结果如图 4.4 所表明，模型检测器一直运行，检测执行及关闭时没有抛出异常，说明规约没有
【参考文献】：
期刊论文
[1]一种软件定义网络中的控制器热备份及选举算法[J]. 王文博,汪斌强,陈飞宇,王志明,宫阳阳. 电子学报. 2016(04)
[2]基于行为时序逻辑TLA的Pastry协议的规约与验证[J]. 刘照洋,龙士工. 贵州大学学报(自然科学版). 2015(06)
[3]SDN和NFV对网络变革发展影响综述[J]. 张志强. 现代电信科技. 2015(01)
[4]SDN控制器的调研和量化分析[J]. 江国龙,付斌章,陈明宇,张立新. 计算机科学与探索. 2014(06)
[5]基于TLA+的AFDX冗余管理算法的改进[J]. 库恒,龙士工,罗昊. 计算机工程与设计. 2013(03)
[6]基于TLA的ARQ协议描述与验证[J]. 吴勇,李祥. 计算机安全. 2012(08)
[7]分布式超级节点选举算法[J]. 杜丽娟,余镇危. 计算机工程与应用. 2011(14)
[8]ARP协议的描述与TLA验证[J]. 李元,吴勇,李祥. 计算机技术与发展. 2010(06)
[9]基于TLA+的BRP协议规约及验证[J]. 陈立前,王戟,陈火旺. 计算机工程与科学. 2006(01)
硕士论文
[1]PAXOS算法改进及应用研究[D]. 刘春涨.广西民族大学 2016
[2]基于Zookeeper的SDN多控制器架构的研究与实现[D]. 田心宁.兰州大学 2016
[3]基于行为时序逻辑TLA的网络协议的描述与验证[D]. 刘照洋.贵州大学 2015
本文编号：2936149
本文链接：https://www.wllwen.com/guanlilunwen/ydhl/2936149.html
