随着VLSI技术的不断发展，尤其是Dennard缩放定律的终结，单核已经不能满足硬件发展的需求，多核已成为主流的体系结构。多线程技术的提出更加高效地利用了硬件资源，同时也给并行程序设计提出了更高的挑战。多核多线程技术的结合，以及更多跨平台应用的涌现，迫切需要运用并发模型提高软硬件系统开发效率。常见的并发模型如Petri网、广播协议和线程迁移系统等本质上是一种无穷状态系统，并发的特殊性和多样性导致该类系统安全性验证存在状态空间爆炸问题，计算开销和内存开销非常大，实现高效验证非常困难。良拟序结构迁移系统是一大类无穷状态系统的统称，涵盖Petri网、广播协议、有损信道系统和线程迁移系统等并发模型，其安全性验证问题可以归结为可覆盖性问题，并且已被证明是可判定的。
　　本文围绕良拟序结构迁移系统这一大类无穷状态系统的安全性验证问题，提出了几种通过模型检验技术解决无穷状态系统安全性验证的算法。遵循从特殊到一般再回归特殊的研究方法，以Petri网模型描述的参数化系统安全性验证为出发点，进而研究了通用的良拟序结构迁移系统可覆盖性算法，最后聚焦解决多线程程序安全性验证的实际应用问题。本文的主要研究成果及创新点概括如下：
　　(1)提出一种基于Petri网的参数化系统安全性验证算法
　　参数化系统由一组结构相同、并发运行的组件构成，其中组件的个数称之为系统参数。由于组件个数无穷，因而参数化系统本质上是一种无穷状态系统。针对如何提高参数化系统的验证规模，提出一种基于Petri网的参数化系统安全性验证算法。首先，采用计数抽象技术将参数化系统转换为Petri网模型；然后，运行基于SAT求解器的模型检验算法增量式地验证安全属性。通过计数抽象和模型检验技术相结合，进一步提高了参数化系统的验证规模。实验表明，该算法执行速度更快，内存开销更少，参数化协议的验证规模是同类工具TDA的8～10倍。
　　(2)提出一种面向良拟序结构迁移系统安全性验证的不动点计算加速算法
　　针对精确可分割良拟序结构迁移系统的安全性验证问题，提出一种面向良拟序结构迁移系统安全性验证的不动点计算加速算法。该算法以基于BDD的确定状态后向搜索算法为基础，通过运用IC3算法作为启发式引擎计算后向搜索上逼近，加速不动点计算速度，进而快速解决安全性验证问题。实验结果表明，通过运用IC3算法加速不动点计算，提高了问题求解速度，尤其是对于可覆盖(不安全)的例子，计算速度提升是经典的后向搜索算法的100倍以上，内存开销显著降低。
　　(3)提出一种基于后向搜索上逼近的良拟序结构迁移系统安全性验证算法
　　针对良拟序结构迁移系统可覆盖性分析计算成本高的问题，提出一种运用有限状态模型检验技术解决无穷状态系统可覆盖性问题的算法。首先将良拟序结构迁移系统划分为不同权值限定下的一系列有限状态机模型，然后采用IC3算法增量式地计算不同权值下模型的后向搜索可达状态空间上逼近，进而证明系统是否安全。结合IC3算法增量式求解以及并发模型的特点，提出了编码压缩等一系列优化方法，通过修改IC3算法实现细节，提高了求解速度，降低了内存开销。实验结果表明，该算法在同等计算时间限制下能够解决更多的测试样例。在1GB内存限制下，可以解决97.2%的测试样例，超过同类算法的2倍。
　　(4)提出一种面向多线程程序的安全性验证算法和框架
　　针对Pthread类型多线程程序安全性验证问题，结合谓词抽象技术和模型检验技术，提出一种面向多线程程序的安全性验证算法。实验结果表明，该算法比已有的完全算法更快地解决安全性验证问题，而且内存开销更低。同时，提出了一个面向多线程并行程序安全性验证的框架，集成了多个验证引擎，相互配合从而更加高效地完成验证任务。实验表明，采用多个工具相结合的方式，能够高效验证多线程并行程序安全性问题，适用于解决更大规模的实际工程问题。