嵌入式软件静态测试不运行程序，对软件的专用性、实时性和嵌入性依赖度低，因而成为嵌入式软件质量保证和成本缩减的重要措施。软件特性及结构作为重要的测试对象，能够揭示潜在的错误，提高测试的准确度，然而有关软件特性及结构的嵌入式静态测试较少。程序不变量是性质不变的数据合约形式，能够表现软件各变量的关联特性，及时更新软件系统的说明文档、算法、数据结构等方面的信息，还可以确定错误的位置，因此采用程序不变量进行嵌入式软件特性及结构方面的静态测试。本文基于抽象解释理论，提出了一种针对嵌入式C源代码的程序不变量静态获取方法。通过基础分析来构造被测程序的抽象域图；遍历抽象域图进行抽象执行得出被测程序中可执行路径；结合程序不变量的重复性符号化执行可执行路径，获取具有函数关系及集合关系的初始程序不变量。该方法能够有效地解决复杂问题的逼近求解，减少系统的开销。本文在多项式关系与程序不变量联系研究的基础上，提出了程序不变量验测方法。通过被测程序中可执行路径确定多项式程序与最弱前置条件；将初始程序不变量转化成多项式关系；抽象分析多项式关系在多项式程序的目标结点处正确与否，完成程序不变量正确性的验证。通过词法分析、语法分析检测出规范性的静态错误；结合软件需求规格说明或设计文档检测正确的程序不变量，发现数值范围、文档除零等静态错误。该方法剔除了似然程序不变量，提高了检测的正确度和效率。最后，本文利用VC++2005实现了程序不变量静态测试系统，并以嵌入式Linux环境下的实例代码对其进行验证，通过实际结果与预期要求的一致性证明了本系统设计的可行性与正确性。