在软件生命周期中,软件测试是保证软件质量的重要环节之一。软件测试可分为动态检测和静态检测,动态检测是通过测试用例在运行时检测正确性,静态检测则是直接分析源代码。静态检测技术通过强大的抽象解释使分析精确而高效,并且拥有自动化、完善性(完全控制和数据覆盖)等特点,使其在工业环境中成为一种广受欢迎的方法。但随着计算机技术的发展,并发软件已经有了广泛的应用。并发软件的发展给软件测试带来了新的挑战,执行路径的不确定性是并发软件的重要特性,也是测试的难点所在,由于并发状态空间较大,直接将顺序程序的静态检测技术应用于交错执行的并发程序中效果并不好。线程模块化分析方法不用考虑线程交织以及相关的执行构建说明,可以通过分别分析每个线程来实现对并发程序的验证。线程模块化分析方法的主要优势在于可以用最小的代价将顺序抽象解释器提升为并发抽象解释器。该方法的核心思想分做两个步骤:首先,创建线程,并将所有的线程作为一个独立的顺序程序进行分析,同时收集其他线程对其变量的影响。然后,重新分析所有的线程,并且计算线程间的干涉,保存发现的新的行为和新的可能的干涉。递归这个过程直到干涉稳定。但传统的线程模块化分析方法是基于线程交互的非关系型流不敏感的具体语义,分析更容易处理但结果不是很准确,本文在线程模块化分析方法的基础上实现了线程间的流敏感并提出了一种基于数据流图的约束,使分析结果更加准确。本文主要创新点如下:1.在原始模块化分析方法的基础上,我们提出了一种基于抽象解释的流敏感的线程模块化分析方法,使分析更加准确。2.我们开发了一种轻量级的基于数据流图的约束框架,用于检测线程内的干涉是否有效,以提高分析效率,提升分析精度。3.在上述理论研究支持下,我们基于这种算法开发了一个面向嵌入式并发程序的分析工具原型。4.以验证航空发动机控制系统为例,通过应用我们的线程模块化分析方法对系统进行了静态检测,展示了算法对嵌入式并发程序分析与验证的能力。