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