基于云计算平台的形式化技术相关并行查询与检测算法的研究

发布时间：2021-06-11 06:57

　　随着计算机软硬件体系的发展,能够确保其安全、可靠的形式化验证成为研究热点。其中,模型检测作为一种用来验证有限状态系统是否满足形式化规范的高度自动化的验证方法,备受关注。但是随着形式化方法的发展,约束规则的增加以及状态空间的复杂,如何更好地提高大规模约束规则查询的速度,保证具有复杂状态的模型检测的效率,已经成为一个迫切需要得到解决的问题。在形式规约方面,面对大规模约束查询,基于单节点的约束查询方法已经无法高效地完成大规模的查询任务,例如对象约束语言的约束查询效率过低问题。在形式验证方面,面对复杂系统模型检测,可能导致状态爆炸问题,例如计算树逻辑模型检测状态爆炸问题。相关研究表明可以利用云计算平台,解决上述形式化方法面临的问题,保证相关查询以及验证算法的效率。在此基础上,本文为了应对大量约束查询带来的挑战,提高OCL查询的速度,提出了一种基于MapReduce的OCL并行查询方法。这种方法通过提取OCL对象属性集合,实现从OCL规则库查询到OCL对象属性查询的转化,并利用MapReduce实现对象属性并行查询,缩短了OCL查询时间。实验结果表明,利用MapReduce实现对象属性并行查询,... 

【文章来源】：南京邮电大学江苏省

【文章页数】：66 页

【学位级别】：硕士

【部分图文】：

XML文档片段其中第一个和中间的部分是一个对象属性，在该片段中表示一个Owner(车主对象)

图 3.5 Owner 特征集合CL 并行查询处理CL 并行查询输入的数据实际上是 OCL 对象属性集合。根据上一小节可知，Extra据标签对从OCL规则库中获得符合条件的OCL片段，并组合成了OCL对象属性集预处理后，OCL 并行查询剩下的工作就是对对象属性进行筛选并获取结果，需要查询情况建立对应的 MapReduce 任务。在 MapReduce 任务中，Mapper 或 Reduc理的对象属性，是以流的形式传递进来的。在 Map 函数之后，还会有一个洗牌(shu之后才会进行相应的 Reduce 任务进行最终结果的构建。个 OCL 并行查询包括对象属性筛选和构造查询结果两部分。OCL 查询会被处理干个 MapReduce 任务，每个 MapReduce 任务可以处理一个或多个查询条件，以象属性。最后，将筛选出来符合查询条件的对象属性进行结果构造，得到最终的结

【参考文献】：
期刊论文
[1]分布式XML Twig查询处理方法[J]. 何志学,廖湖声,王静.  计算机工程与设计. 2016(01)
[2]一种基于GPU的快速XPath查询算法[J]. 黄玉龙,苏本跃,奚建清.  计算机应用与软件. 2016(01)
[3]基于MapReduce的XML结构连接处理[J]. 李东,邓泽航,李祖立.  计算机科学与探索. 2016(08)
[4]基于多谓词选择的海量XML数据并行查询方法[J]. 闫威,马宗民.  小型微型计算机系统. 2015(07)
[5]Hadoop迭代优化技术的研究[J]. 王晓军,邹亮亮.  计算机技术与发展. 2014(09)
[6]MapReduce并行计算技术发展综述[J]. 应毅,刘亚军.  计算机系统应用. 2014(04)
[7]一种改进的大规模CTL公式检测算法[J]. 奚琪,王清贤,曾勇军,秦艳锋.  计算机科学. 2013(10)
[8]MapReduce并行编程模型研究综述[J]. 李建江,崔健,王聃,严林,黄义双.  电子学报. 2011(11)
[9]云计算:体系架构与关键技术[J]. 罗军舟,金嘉晖,宋爱波,东方.  通信学报. 2011(07)
[10]云计算和虚拟化技术[J]. 张耀祥.  计算机安全. 2011(05)

博士论文
[1]实时服务构件的语义特征和行为组装形式化技术研究[D]. 金仙力.北京邮电大学 2008

硕士论文
[1]基于云计算平台的时态逻辑模型检测算法研究与实现[D]. 段廷银.郑州大学 2016
[2]基于OCL和AOP的面向对象软件系统行为监控与验证研究[D]. 王晓曦.北京工业大学 2014
[3]形式化B方法验证技术研究及其应用[D]. 滕腾.扬州大学 2008
[4]基于XML描述的软件设计模式实例化研究[D]. 陈贤谋.湖南大学 2005



本文编号：3224059