基于概率模型检测的分布式算法验证和分析

摘要

分布式算法在实际应用中具有重要的价值意义,本文采用一种基于概率模型检测技术验证和分析了两类分布式算法的性质,并这些性质给出了相应的证明。由于概率模型检测可以穷举状态空间,相比于传统方法,使得它更接近真实应用环境,更利于我们研究算法的安全性和有效性;同时概率模型检测器中的马尔科夫技术可以分析出模型中那些不确定因素。
　　随机分布式算法中有一种自动恢复状态的算法—自稳定算法, Mitchell Flatebo提出的自稳定算法是通过一个简单随机的解决方案解决n个进程令牌环中的故障,使故障自动恢复正常。他证明出最坏的情况有n-1个令牌,所需要的时间的上界是0.5N2-0.5N-2。从实验中,发现这个上限出现的可能很小。而在实际应用中,我们更注重系统预期恢复稳定状态的时间—预期最差时间。实验中,主要采用PRISM工具验证了Flatebo算法的性质,并且把它与同类型Herman自稳定算法做了比较,当系统中的结点数目增加时,它的性能会逐渐提高,优于Herman算法;另外,还用线性回归从实验结果中拟合出预期最差时间在O(N1.45)和O(N1.47)之间;最后还给出一个验证和分析自稳定算法的简单方法。
　　本文研究的另一个分布式算法是随机互斥算法,提出了一个基于概率模型检测工具PRISM方法,用于验证和分析Kerry Raymond提出的分布式K互斥算法,首先验证了互斥算法无死锁和无饥饿两种基本性质;然后通过PRISM验证某一进程进入临界区平均及时时间;接着分析我们的实验结果,当各个进程的相对访问临界区资源的时间相差不大时,增加临界资源 k的数量,不能很明显提高进程的平均及时时间,但如果其中某一进程访问临界资源的时间较长,那么增加 k的值,就会大大提高运行效率。随后我们通过添加额外的存储结构,获得了新的改进 k互斥算法,可以大大降低进程之间的发送和接受延时。最后给出改进的k分布式算法。

目录

封面

声明

中文摘要

英文摘要

目录

第1章 引言

1.1研究背景和意义

1.2 概率模型检测的研究现状

1.3 分布式算法

1.4 研究的内容和贡献

1.5 论文结构

第2章 概率模型检测

2.1 引言

2.2 概率模型

2.3 概率模型时序逻辑

2.4 模型检测马尔科夫链解决方法

2.5 模型检测工具PRISM

2.6本章小结

第3章 Flatebo算法建模验证和分析

3.1 引言

3.2 自稳定算法

3.3 Flatebo算法简介

3．4 Flatebo算法的概率验证

3.5 本章小结

第4章 Kerry算法建模验证和分析及其改进算法

4.1 引言

4.2 Kerry算法建模

4.3 Kerry算法验证

4.4 Kerry算法分析和证明

4.5改进k互斥算法

4.6 本章小结

第5章 结论

5.1 研究总结

5.2 进一步开展的工作

参考文献

致谢

个人简历、在校期间发表的学术论文与研究结果