陈立前， 吴国福， 姜加红

1. 国防科技大学计算机学院， 湖南 长沙 410073 2. 国防科技大学空天科学学院， 湖南 长沙 410073 3. 北京跟踪与通信技术研究所， 北京 海淀 100095

0 引 言

随着我国卫星、大运载火箭、载人航天、探月计划的发展，航天嵌入式软件的规模和复杂程度日益增大，系统并发性不断增强，软件系统变得日趋庞大和难以驾驭，软件系统中潜在的缺陷也越来越难以检测、定位和控制[1].软件故障已成为航天系统失败的重要因素[2].源代码级程序错误仍是航天嵌入式软件中最突出的问题之一，数组越界、算术溢出、被零除、空指针解引用、数据竞争等问题仍经常发生.

静态分析是一种在编译时通过分析程序源代码来推断程序运行时性质的程序分析技术，是检测代码缺陷、提高代码安全性与可靠性的一种重要技术.尽管程序分析是一类不可判定问题，然而通过适当的抽象，静态分析能够构造程序行为的某种近似，并得出有意义的分析结果.程序静态分析的目标是在程序运行前尽可能多地发现其中隐含的错误，以提高程序的可靠性和安全性.对于一些常见的源代码级程序错误，虽已有较成熟商业化静态分析工具(如Coverity、Klocwork、Parasoft等)支持其检测，但是这些工具主要基于语法规则、缺陷模式等开展分析，程序语义信息利用不够，且对于航天嵌入式软件中常见的中断并发机制、浮点运算、面向可靠性的容错设计等代码特征和要素考虑不够，因此这些工具还不……