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

发布时间：2021-08-03 15:49

　　模型检查是一种非常重要的形式化验证技术,它利用状态空间搜索来探索所有可能的系统状态。以这种方式,可以检查给定的系统是否满足某些属性。近年来,模型检查得到了快速的发展,已经在很多高安全性领域中得到了广泛应用,如航空航天、轨道交通、汽车电子、工业控制等领域。下推系统因其特殊的结构,是模型检查中一种常用的理论模型。下推系统的模型检查已广泛应用于程序分析、恶意软件检测等实际问题。可是,在现实问题中,仍然有一些问题限制着模型检查技术的发展。首先,随着程序的复杂化,模型检查遇到的一个真正的挑战,就是众所周知的状态爆炸问题。其次,现有模型检查算法的效率往往取决于状态空间的大小,在有限的处理器和内存条件下,更加有效地进行模型检查也变得困难重重。到目前为止,已经出现了一些技术来解决以上的问题,如:符号模型检查、偏序规约、对称规约等技术。除了这些传统的技术外,并行计算,尤其是,在大规模计算任务方面表现出了独特的优势,这引起了模型检查研究者的广泛关注。一些工作已经使用对模型检查进行加速,并且取得了不错的效果。本文基于自动机理论,为下推系统的模型检查提出了通用并行解决方案,并基于实现了下推系统可达性分析和模型... 

【文章来源】：华东师范大学上海市 211工程院校 985工程院校 教育部直属院校

【文章页数】：95 页

【学位级别】：硕士

【部分图文】：

图一个示例程序

【参考文献】：
期刊论文
[1]工业4.0和智能制造[J]. 张曙.  机械设计与制造工程. 2014(08)
[2]利用GPU进行通用数值计算的研究[J]. 徐品,蓝善祯,刘兰兰.  中国传媒大学学报(自然科学版). 2009(02)
[3]基于图形处理器（GPU）的通用计算[J]. 吴恩华,柳有权.  计算机辅助设计与图形学学报. 2004(05)
[4]基于形式化方法的需求分析[J]. 塔维娜,何积丰.  计算机工程. 2003(18)
[5]软件可靠性研究与进展[J]. 刘云,赵玮.  微机发展. 2003(02)



本文编号：3319892