随着多核处理器和并发技术的快速发展,并发多线程程序设计成为了软件开发的主流模式,并发系统被逐渐应用于多个领域,为人们的生活提供了诸多便利。然而,并发系统的结构一般比较复杂,且存在多个线程相互交错执行的情况,传统的模拟和测试方法难以发现系统中的微小错误。通常采用模型检测验证并发系统的正确性,但并发系统的状态空间随着并发量的增加呈指数级增长,严重制约了模型检测的验证效率。谓词抽象技术能够有效地缓解状态空间爆炸问题,对源程序实施谓词抽象可以产生布尔程序,布尔程序作为程序验证的简单模型,在一定程度上优化了状态空间,提高了模型检测的验证效率。本文以无界线程的并发布尔程序为研究对象,分析程序中违背断言的状态是否可达,具体工作内容如下:(1)研究了后向搜索算法的基本流程,分析了算法的搜索策略和最小覆盖前驱的计算方法,并结合并发布尔程序的特点,提出一种深度优先的后向搜索算法,对最小覆盖前驱的计算方法进行优化,提高了并发布尔程序可达性分析的效率。(2)研究了并发布尔程序的线程迁移系统,在改进的算法基础上,结合计数器抽象技术和summarization方法,提出了一种基于线程迁移系统的可达性分析模型。采用向上逼近的方式对并发布尔程序的线程迁移系统进行扩展,并反向分析扩展线程迁移系统中的每一条路径,通过数学公式描述路径中所有状态迁移对局部状态线程计数器的影响,找到一条使数学公式成立的路径,从而验证并发布尔程序状态的可达性。(3)对本文提出的基于线程迁移系统的可达性分析模型的三个核心模块,包括扩展迁移模块、公式求解模块和搜索算法模块进行了具体的设计和实现,并对该模型的正确性和分析效率进行了验证。本文提出的基于线程迁移系统的可达性分析模型能够正确和高效地分析并发布尔程序的状态可达性,从而完成对并发程序的正确性验证。