基于概率模型检测的动态系统领导者选举协议分析与验证

《基于概率模型检测的动态系统领导者选举协议分析与验证》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、中图分类号：TP311论文编号：102871616-SZ028学科分类号：085212硕士学位论文基于概率模型检测的动态系统领导者选举协议分析与验证研究生姓名顾佳仪专业类别工程硕士专业领域软件工程指导教师周宇副教授南京航空航天大学研究生院计算机科学与技术学院二О一六年一月NanjingUniversityofAeronauticsandAstronauticsTheGraduateSchoolCollegeofComputerScienceandTechnologyAnalyzingandVerificationofLeaderElectionProto

2、colinDynamicSystemsviaProbabilisticModelCheckingAThesisinSoftwareEngineeringbyJiayiGuAdvisedbyAssociateProf.YuZhouSubmittedinPartialFulfillmentoftheRequirementsfortheDegreeofMasterofEngineeringJanuary,2016承诺书本人声明所呈交的博/硕士学位论文是本人在导师指导下进行的研究工作及取得的研究成果。除了文中特别加以标注和致谢的地方外，论文中不包含其他人已经发表

3、或撰写过的研究成果，也不包含为获得南京航空航天大学或其他教育机构的学位或证书而使用过的材料。本人授权南京航空航天大学可以将学位论文的全部或部分内容编入有关数据库进行检索，可以采用影印、缩印或扫描等复制手段保存、汇编学位论文。（保密的学位论文在解密后适用本承诺书）作者签名：日期：南京航空航天大学全日制专业学位硕士学位论文摘要领导者选举协议是分布式计算中的重要协议。它能够保证分布式系统选举出唯一的领导者，使之协同系统中其余进程的工作，以此提高整个系统的工作效率。随着动态系统逐渐成为分布式计算的研究热点，在该系统中的领导者选举协议的设计和验证获得较多的关注。对

4、于该协议的验证，必须立足于动态系统。由于动态系统中包含了很多不确定的因素，这给传统的基于模型检测的协议验证方法带来了很大的挑战。本文采用概率模型检测技术，对这种广泛存在的不确定性进行建模，围绕着动态系统中的领导者选举协议进行了较为系统的分析，并应用主流开源概率模型检测工具PRISM对最近提出的层次式领导者选举协议进行建模与验证。（1）在模型分析的过程中，针对模型检测领域常见的“状态爆炸”问题，本文通过简化协议的内部操作，删除多余步骤，来减少模型的状态数。对其中不确定的行为，通过为其设定概率系数，取代原先复杂的条件判定操作，从而缓解了模型状态爆炸问题的产生

5、。（2）在模型构建的过程中，引入了“假设-保证”的组合式验证思想，将层次式协议进行分别处理，建立了一个具有双层结构的领导者选举协议模型，并通过实验，给出了具体验证结果，显示了该模型的有效性。（3）在整个实验的过程中，针对模型中含有大量相似的内容造成代码重复书写的问题，本文提出了一种自动生成PRISM代码的方法，在很大程度上提高了代码的编写效率。并且借助于C语言，完成了简易的PRISM代码自动生成的脚本程序。本文的研究意义在于对近期提出的层次式领导者选举协议进行了分层建模与验证，验证模型的规模和效率比传统的整体式验证都有了很大的提升，为动态系统中领导者的确

6、定，提供了一种比较合理的方法，增强了动态系统的工作效率。关键词：形式化验证，概率模型检测，领导者选举协议，动态系统I基于概率模型检测的动态系统领导者选举协议分析与验证ABSTRACTLeaderelectionprotocolisoneofimportantprotocolsindistributedcomputing.Itcanguaranteeauniqueleaderofthedistributedsystemtobeelectedforsakeofcoordinatingotherprocessesandthusimprovetheproduct

7、ivityofthewholesystem.Withtheincreasingdevelopmentofthedynamicsystemwhichhasgraduallybecomeahottopicindistributedsystem,leaderelectionprotocolsinsuchcontexthaveattractedmoreandmoreattention.Sincetheinherentuncertaintraitsofthedynamicsystems,thetraditionalapproachesofmodelchecking

8、arefullofgreatchallenges.Accordingtothel