您现的位置:首页 > 数据库检索 > 中文会议 

一种基于CUDA的面向下推系统的并行模型检查方法

加收藏
  • 【题名】:一种基于CUDA的面向下推系统的并行模型检查方法
  • 【年份】:2020
  • 【作者】:魏汉生
  • 【关键词】:并行计算  模型检查  下推系统  GPU  LTL
  • 【摘要】:模型检查是一种非常重要的形式化验证技术,它利用状态空间搜索来探索所有可能的系统状态。以这种方式,可以检查给定的系统是否满足某些属性。近年来,模型检查得到了快速的发展,已经在很多高安全性领域中得到了广泛应用,如航空航天、轨道交通、汽车电子、工业控制等领域。下推系统因其特殊的结构,是模型检查中一种常用的理论模型。下推系统的模型检查已广泛应用于程序分析、恶意软件检测等实际问题。可是,在现实问题中,仍然有一些问题限制着模型检查技术的发展。首先,随着程序的复杂化,模型检查遇到的一个真正的挑战,就是众所周知的状态爆炸问题。其次,现有模型检查算法的效率往往取决于状态空间的大小,在有限的处理器和内存条件下,更加有效地进行模型检查也变得困难重重。到目前为止,已经出现了一些技术来解决以上的问题,如:符号模型检查、偏序规约、对称规约等技术。除了这些传统的技术外,并行计算,尤其是,在大规模计算任务方面表现出了独特的优势,这引起了模型检查研究者的广泛关注。一些工作已经使用对模型检查进行加速,并且取得了不错的效果。本文基于自动机理论,为下推系统的模型检查提出了通用并行解决方案,并基于实现了下推系统可达性分析和模型检查的加速。本文的主要贡献概括如下1.提出了两个多线程模型:多线程下推自动机和多线程下推系统。基于自动机理论,本文深入分析了下推系统模型检查算法的执行过程,将原有模型扩展为支持多线程的模型。这两个多线程模型,为在多线程并行框架中表示下推自动机和下推系统提供了新的思路。2.提出了基于下推系统的并行模型检查算法。并行算法包括:并行的正向可达性分析算法、并行的逆向可达性分析算法和并行的模型检查算法。并行算法将模型检查的计算任务分配到多线程上执行,从而为下推系统的并行模型检查提供了新的解决方案。此外,本文提出的并行算法为通用算法,可以在多种多线程并行架构上进行实现。3.设计并实现了基于下推系统的并行模型检查工具。该工具基于实现,可以利用主流的多线程对下推系统的可达性分析和模型检查进行加速。该工具使用特殊的数据编码方式和动态任务管理,取得了良好的加速效果。实验结果显示,本文提出的并行方法比现有模型检查方法可以更加有效地解决下推系统的模型检查问题。最快可以获得倍左右的加速效果。
  • 【会议名称】:硕士
  • 【类别名称】:史建琦
  • 【载体】:华东师范大学
  • 【会议地点】:2020
相关文献
一种基于软件方法容错架构设计和实现
基于Logistic回归模型航天器健康状态评估方法
一种阻抗匹配射频电子学系统非破坏性检测评估方法研究
一种基于多浮标无源水下导航定位方法
一种基于模糊理论机会信号测距性能综合评估方法
面向TC-OFDM系统基于压缩感知PMF-FFT捕获算法
一种基于微分求积升阶谱有限元方法正交有理金字塔基函数
一种基于改进MEDLL方法GNSS信号畸变参数估计方法
一种基于北斗智能轮式载体定位定姿测速方法
基于导航系统多优先级星间链路时隙规划方法研究
获取此文方式
登录后才能存到网盘,
请登录
下载请求:
   

说明:点击”存到网盘“按钮即收取费用,重复点击不收费,如果下载失败,我们会自动转为文献传递方式处理,稍侯请关注您网盘上该文献的信息,从网盘上下载该文献不用重新付费。