第一章 绪论
1.1背景
近年来，随着计算机科学技术的飞速发展，计算机硬件和软件系统在人们的生活中起着越来越重要的作用。人们对计算机软硬件系统的可靠性和安全性的要求也越来越高 。对于一些高安全性行业，例如航空航天、轨道交通、汽车电子、工业控制等，如果系统在投入使用之前没有经过可靠的安全认证，则可能会导致一些不可估量的后果。即使系统中的一些错误并不致命，但如果能提前找到它们，
就可以对系统及时地进行更正，减少一些不必要的损失。因此，如何确保计算机系统的正确性和可靠性变得越来越具有挑战性，这也是学术界和工业界一直密切关注的问题之一。
经过近几?年来世界各国研究者的不懈努力，软件测试和形式化验证 已成为目前软件开发过程中两种分析软件安全性和可靠性的重要方式。软件测试是指在软件开发完成后，给定输入和所期望的输出，通过人工或者自动化软件根据每一步的执行情况来检验所开发的软件是否满足开发需求和预期结果的过程。软件测试的缺点是不够完备，当存在无限种输入输出时，人们不可能在有限的时间里穷尽所有的情况。在实际的软件开发过程中，软件的功能变得越来越复杂，软件测试者有时无法确定输出的正确性。此外，软件测试只能断言是否存在错误，也不能解释错误的原因。因此，软件测试并不能完全保证软件的正确性。
形式化验证的出现就是为了解决以上这些问题。形式化验证使用数学的方法可以充分地证明或验证软件的正确性。模型检查是研究者常用的一种自动形式化验证方法，它主要用于软件和硬件系统的静态分析和验证，可以在不运行程序的情况下确定系统是否满足某些特定属性。基于此特性，该技术在很多软件工程的开发中起着至关重要的作用，例如硬件、软件、通信协议、控制系统和安全认证协议。因为它比抽象解释、定理证明等其他形式化验证方法更完整，所以它已经应用于恶意软件检测、二进制程序分析、属性检查和其他验证方法。
..........................
1.2研究目的与意义
由上述可知，模型检查是用于形式化验证硬件和软件模型正确性的关键技术，可以自动地探索系统模型的状态空间，在高安全要求领域中的设计阶段起着重要的作用。在国家工业4.0的背景下，我国也迫切需要能够保证工业控制软件的安全性和可靠性的技术。而下推系统因其独特的栈属性，在模型检查中越来越受研究者的欢迎。在恶意代码检测和数据流分析等领域，下推系统的应用已经取得了显著的成果。然而，随着系统状态变量或过程数量的增加，下推系统状态空间的大小呈指数增长，这导致了状态空间的爆炸问题。状态空间的爆炸导致模型检查器需要大量的计算资源去完成单个模型检查的任务，因此传统的方法对大型工业系统的适用性相当有限。目前，MOPED是现存的一个比较流行的下推系统模型检测器，但是它是在CPU上串行执行计算任务的，当要检查的模型比较复杂时，MOPED需要几个小时甚至几天的时间进行运算，这样的效率是让人无法忍受的。为了应对越来越复杂的模型，我们迫切地需要更加高效的下推系统模型检查解决方案。
改进模型检查效率的一个方法是利用现代并行架构的计算能力。GPU具有巨大的并行能力，它可以并行运行数万个线程，在加速模型检查方面具有很大的潜力，可以提高几个数量级的加速。本文在传统下推系统模型检查方法的基础上，提出了两个并行模型：多线程的下推自动机和多线程的BUCHI下推系统，然后基于传统可达性算法提出并行的下推系统可达性算法，并将并行可达性算法应用于LTL 模型检查中。此外，为了充分发挥CPU 的性能，本文为下推系统提出了新的编码方式和动态任务管理。实验表明，本文的并行方法在时间效率方面取得了显著的加速，并且在空间利用率上也取得了良好的效果。本文的方法可以对下推系统进行高效的验证，为下推系统的模型检查提供了新的解决方案。在工控安全，病毒软件检查，数据流分析等领域，该方法都能发挥巨大的价值，为下推系统模型检查工作节省大量的资源。
.............................
第二章 基础知识
2.1迁移系统
迁移系统是一种最常见的形式化验证模型，它可以自然地捕捉离散系统的动态行为。为了对一个系统的行为进行建模，可以把该系统看做一个拥有不同状态的实体。然后可以用数学的形式描述系统的所有状态以及状态之间的迁移关系。标记迁移系统是一种用于系统行为建模的基本模型，广泛应用于计算机辅助设计和形式化验证。下面给出标记迁移系统的定义：
..........................
2.2传统的模型检查方法
在模型检查中，可达性分析是一种非常重要的技术。绝大多数系统的安全性和活性可以使用可达性分析算法进行模型验证。可达性的一种重要的应用就是LTL模型检查问题。本节将详细地介绍传统的基于下推系统的可达性分析和LTL模型检查问题及方法。
由上文可知，下推的系统的可达性分析两种方法的输入都是一个下推系统和一个下推自动机，然后根据下推系统的迁移规则和下推自动机的迁移，不断地应用饱和规则给下推自动机添加新的迁移，直到没有新的迁移可以添加，即达到下推自动机的稳定状态。这个过程是一个反复迭代的过程，很多学者对这一过程进行了优化，目前最常用的方法就是SCHWOON提出的算法。可是他的算法是串行的，每次迭代只能取一条迁移，然后根据这条迁移去检查有没有新的迁移可以添加。而每次迭代添加的新迁移可能有很多个，这就导致遍历迁移的速度跟不上新迁移生成的速度，新迁移越积越多。当模型很大时，新迁移的数量是巨大的，一个个地去遍历效率非常低。
..........................
3.1传统的模型检查方法................21
3.1.1可达性分析................21
3.1.2LTL模型检查................21
第四章 基于CUDA的并行模型检查的设计与实现.....................45
4.1基于CUDA的并行模型检查流程..................45
4.2基于CUDA实现的并行模型检查算法....................45
第五章 应用与实验...................62
5.1并行模型检查工具...................62
5.2程序到下推系统的转换...................62
第五章 应用与实验
5.1并行模型检查工具
下推系统因其独特的结构，是程序分析中一种重要的模型，例如可以将用C或 java等语言编写的程序转化为下推系统，进而对这些程序进行分析验证。一个程序通常由许多函数组成，函数可以通过相互调用将参数值传递给被调用者，或将返回值返回给调用者来进行交互。函数的执行也可能涉及对其他函数的调用，有些甚至涉及到对自身的递归调用。当一个函数终止时，程序会在调用该函数的地方继续执行。
..........................
第六章 结语
6.1工作总结
近年来，我国工业领域飞速发展，尤其在工业4.0的背景下，工业自动化、工业控制等领域迫切需要安全且可靠的软件作为支撑。下推系统的模型检查也被越来越多的学者应用到工业领域中，从而对工业软件进行形式化验证。然而，随着工业软件的规模不断增大，对庞大的工业软件进行模型检查变得具有挑战性。巨大的时间和内存消耗让人无法忍受。好在随着计算机技术的不断发展，并行技术也日新月异，为模型检查提供了新的解决思路。本文基于下推系统，为下推系统的模型检查提供了一种并行解决方案，并将此方法应用于真实的模型检查上，最终取得了良好的效果。
为了并行地解决下推系统的模型检查问题，本文深入研究了下推系统模型检查的相关理论知识，基于传统模型检查方法，从模型，算法，数据结构，任务管理等方面着手，提出了并行的下推系统模型检查方法。本文的主要工作如下：
（ 1） 提出了两个多线程模型：多线程下推自动机和多线程Buchi下推系统。本文根据自动机理论以及多线程并行架构的特性，对原有模型进行扩展，为在多线程并行框架中表示下推自动机和Buchi下推系统提供了新的思路。
（2 ） 提出了基于下推系统的并行模型检查算法。该算法为通用算法，可以在多种多线程并行架构上实现，将计算任务分配到多线程上执行，为下推系统的并行可达性分析和并行LTL模型检查提供了新的解决方案。
参考文献（略）