中断驱动型程序在嵌入式软件中是一类常见的并发实现方式，并且中断驱动程序广泛应用于一些对安全和稳定性要求极高的领域（包括航空航天、汽车电子、医疗设备等）。因此，针对中断驱动型程序的静态分析研究对于提高嵌入式软件的可靠性具有重要意义。　　已有静态分析技术主要面向顺序程序或通用多线程程序，但是中断驱动型程序有自身的特点，比如：中断与任务之间的打断非对称，中断程序往往具有较强的实时性要求，中断程序的同步方式比较特殊等。使用已有的面向顺序程序的分析方法对中断程序进行分析可能会导致分析结果不可靠。另一方面，使用已有的多线程程序的分析方法对中断程序进行分析，可能会导致分析结果不精确。因此，亟需研究专门针对中断驱动型程序并适合其应用特点的自动化分析方法和工具。　　本文主要研究面向中断驱动型程序的静态分析，研究目标包括：研究中断驱动型程序的顺序化方法，使得顺序化后的中断驱动型程序适合于静态分析；面向顺序化后中断驱动型程序的特点，设计新的抽象域以实现对顺序化后中断程序的分析精度和分析效率取得较好的折衷；针对顺序化后中断驱动型程序的特点，优化过程间分析的效率。本文的主要工作如下：　　1）提出了一种基于数据流依赖的中断驱动型程序的顺序化方法，该方法考虑了中断驱动型程序的特点，即中断与任务之间抢占执行的非对称性，将中断与任务在一个栈中执行，从而实现对中断驱动型程序的顺序化。同时为了尽可能少的引入中断，本文定义了中断之间的数据流依赖，并在需要考虑中断影响的语句处仅考虑对该语句产生影响的中断的集合，从而实现在保证顺序化程序的可靠性前提下，尽可能少的引入中断函数。另外，由于中断驱动型程序中往往使用中断屏蔽字寄存器（IMR）对中断与任务的执行进行同步，本文使用轻量级的位向量抽象域对中断驱动型程序的各个程序点处的IMR取值进行了分析，并利用该分析结果指导实际的中断驱动型程序的顺序化，同时考虑IMR对数据流依赖的影响，确保顺序化后的程序的可靠性。　　2）设计了两个针对中断驱动型程序特征的抽象域：标志量抽象域和语法等价抽象域，以提高分析顺序化后中断驱动型程序的精度。本文针对中断驱动型程序中存在的一类特殊中断：一次发生中断，即一次任务周期内至多发生一次的中断，考虑对该中断的发生情况进行状态划分，以实现对这类中断程序的更精确分析。另外，由于中断驱动型程序中包含有一类代码模式，这类模式会导致使用已有的非关系型抽象域会得到不精确的分析结果。已有的（弱）关系型抽象域能够对该类代码模式得到较为精确的分析结果，但由于其计算代价较高，而在实际大规模程序中并不适用，因此本文基于程序中存在的语法等价关系，设计了能够发现顺序化后的中断程序中存在的语法等价关系，并利用该语法等价关系提升数值分析的精度。　　3）提出了一种面向顺序化后中断驱动型程序的过程间分析优化技术，以提高分析顺序化后中断驱动型程序的可扩展性。顺序化后的中断驱动型程序往往包含大量的中断函数的调用，已有的分析方法对于这些大量函数调用会产生较差的分析效率。为了解决此类问题，本文针对顺序化后中断驱动型程序包含较多中断函数调用的特点，对过程间分析方法进行优化，主要思想是针对不同类型的中断使用不同的过程间分析方法，如复杂中断处理函数使用基于缓存的过程间分析方法，而对于简单中断处理函数则使用基于输入划分的过程间分析方法。以实现在保证一定分析精度的前提下，尽可能的提高分析的效率。　　本文提出的中断驱动型程序数值性质分析方法，在分析精度和分析效率间都做了不同的权衡，可以适用于不同类型的中断程序。目前这些技术已经在抽象解释分析工具框架中得以实现，已在工业界应用中发现多个真实错误。