基于云计算平台的时态逻辑模型检测算法研究与实现

《基于云计算平台的时态逻辑模型检测算法研究与实现》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、学校代码10459学号或申请号201312172060密级硕士学位论文基于云计算平台的时态逻辑模型检测算法研究与实现作者姓名：段廷银导师姓名：周清雷学科门类：工科专业名称：软件工程培养院系：信息工程学院完成时间：2016年5月AthesissubmittedtoZhengzhouUniversityforthedegreeofMasterResearchandImplementationofTemporalLogicModelCheckingAlgorithmbasedonCloudComputingPlatformByTin

2、gyinDuanSupervisor:Prof.QingLeiZhouSoftwareEngineeringSchoolofInformationEngineeringMay,2016学位论文原创性声明本人郑重声明：所呈交的学位论文，是本人在导师的指导下，独立进行研究所取得的成果。除文中已经标注引用的内容外，本论文不包含任何其他个人或集体已经发表或撰写过的科研成果。对本文的研究作出重要贡献的个人和集体，均已在文中以明确方式标明。本声明的法律责任由本人承担。学位论文作者：日期：年月日学位论文使用授权声明本人在导师指导下完成的论文

3、及相关的职务作品，知识产权归属郑州大学。根据郑州大学有关保留、使用学位论文的规定，同意学校保留或向国家有关部门或机构送交论文的复印件和电子版，允许论文被查阅和借阅；本人授权郑州大学可以将本学位论文的全部或部分编入有关数据库进行检索，可以采用影印、缩印或者其他复制手段保存论文和汇编本学位论文。本人离校后发表、使用学位论文或与该学位论文直接相关的学术论文或成果时，第一署名单位仍然为郑州大学。保密论文在解密后应遵守此规定。学位论文作者：日期：年月日摘要摘要通过对动态、并发和实时系统的形式化验证保证其安全性已经成为近几十年来软件工程研

4、究的焦点。由EdmundM.Clarke，AllenEmerson和JosephSifakis等人在20世纪80年代提出的模型检测是一种著名的软件形式化验证技术，它主要通过显式的系统状态搜索或者隐式的不动点计算自动地验证通信协议或者软件系统的模型是否满足要求的规格。模型检测由于其高度自动化而在工业界备受欢迎，提出者也因此在2007年荣获图灵奖。但是模型检测的状态空间随着系统组件的增加成指数增加。这个问题被称为状态空间爆炸问题。如何解决这个问题是当前科学家和学者的研究热点。在大数据和互联网+的时代背景下，云计算日新月异地迅速发展

5、。云计算通过虚拟化技术扩展计算所需的软硬件资源，很大程度上提高了计算机的计算能力，也为应对模型检测的状态空间爆炸问题提供了新的可能的解决方案。本文首先对基于时态逻辑的模型检测技术的国内外研究现状进行了总结。然后，本文分别对云计算和大数据的起源和发展进行了深入研究，从而充分了解了云计算的发展现状和应用背景。不同的云计算的平台通常基于不同的模型实现并行分布式计算，并不能直接用于模型检测，并且通常还需要重新分析相应的问题。这是本文要研究和解决的问题。目前基于云计算平台的模型检测方法主要应用实现了并行计算模型MapReduce的云计算

6、平台Hadoop。然而，Hadoop被设计用来解决大数据的批处理问题，对迭代计算支持的欠佳。而时态逻辑模型检测方法可以归约为图计算，在计算的过程中通常存在多次迭代，基于Hadoop的模型检测方法往往具有较高的延迟。针对以上问题，本文提出了基于BSP消息传递模型的时态逻辑模型检测方法，设计了基于云计算平台Giraph的模型检测器的系统模型并实现了其伪分布式模式。在相同硬件情况下的对照实验表明本文提出的方法很大程度上优于基于Hadoop的方法。这是本文的主要创新点。上述所做的工作，进一步完善了基于云计算平台的模型检测理论体系和技术

7、范畴。关键字：时态逻辑模型检测云计算HadoopGirpahMapReduceBSPIAbstractAbstractToensurethesecuritybyformalverificationofdynamic,concurrentandreal-timesystemshasbeenthefocusofsoftwareengineeringresearchforseveraldecades.ModelcheckingproposedbyEdmundM.Clark,AllenEmersonandJosephSifakisin

8、theeightiesofthe20thcenturyisadistinguishedformalverificationtechnology,whichautomaticallyverifieswhetherthecommunicationprotocolorthesyst