高 猛，滕俊元，陈 睿，孙 民

0 引 言

我国新一代航天器中广泛采用软件密集系统(software-intensive system)，软件在保证航天器安全稳定运行、可靠完成任务方面起着至关重要的作用.航天器许多关键任务的完成均依赖于软件，软件规模和复杂度呈几何级增长，这种特点和趋势在空间站、载人航天、深空探测等重大航天工程中尤为凸显.

同时，航天器属于典型的安全苛求系统，软件一旦发生失效，将会导致任务失败或人员伤亡.例如，某飞控软件由于未及时清除喷气标志导致发动机持续喷气，险些导致火箭发射失利.经统计，近十年五院航天器在轨首次异常中软件因素约占15%、在研质量问题中软件因素约占20%，航天器软件质量问题频发且呈上升趋势.软件安全性已成为航天型号任务中最为关键的风险因素之一.

另外，随着航天器软件缺陷数据的逐步积累，如何利用这些缺陷数据提高软件可靠性安全性是软件从业人员必须思考的问题.典型多发问题的规避和检测是实现软件质量提升的重要途径.统计表明，绝大多数航天器软件问题都是已知类型的缺陷模式[1-2]，符合“二八原则”规律，即约80%的问题分布于20%的缺陷类型中，如时序冲突问题、数据竞争问题、可靠性设计问题、数据取值范围相关问题(如数组越界、除零、数据溢出、变量未初始化等)等.

本文通过系统分析和总结航天器软件典型多发问题，开展软件缺陷模式研究，建立航天器软件缺陷模式集；研究缺陷模式的形式化规约和自动检测技术，开发缺陷模式自动检测工具，提高缺陷检出率，从而有效规避型号中的典型多发问题，提高航天器软件研制质量、缩短研制周期.

1 软件缺陷模式研究

软件缺陷是生存周期内所有存在于软件(文档、数据、程序)之中不正确的，或者是不可接受的需求、设计、编码和数据结构等.而软件缺陷模式[3]是指对特定类型的重复或者类似的软件缺陷的抽象描述，是从实践经验中精炼、抽象而出的缺陷类型.目前传统的软件缺陷分类体系[4](如IEEE软件异常分类、Thayer分类标准、缺陷正交分类ODC标准等)不针对某类具体软件开发语言进行划分，具有良好的通用性，但由于其缺陷抽象程度较高，且缺乏具体实例的支持，具有一定的使用难度.因此，需要结合上述分类方法的优点并结合航天器软件特点，对航天器软件缺陷模式分类，为软件缺陷的检测、定位、修复以及预防提供准确完整的信息.

1.1 缺陷模式获取

航天器软件缺陷数据来源及获取主要有2个方面：

a) 型号在轨/在研软件质量问题和研制过程中出现的典型问题；

b) 型号软件第三方测试问题.

针对上述缺陷数据处理过程如图1所示，首先对缺陷数据进行清洗，将不完整的缺陷描述或错误的缺陷描述尽量给予修复，修复不了的从数据源中剔除；其次根据缺陷产生原因及特性对软件缺陷进行按类划分构成缺陷数据库；之后，采用统计的方法，对缺陷数据库进行统计合并，相同类型的缺陷合并；最后，从重复的、类似的缺陷数据中抽象出缺陷模式.

图1 航天器软件缺陷模式获取流程图Fig.1 The flow chart for obtaining defect pattern of spacecraft software

1.2 缺陷模式描述

为了更好地定义软件缺陷模式，便于软件人员理解和应用，对软件缺陷模式进行规范化描述.本文从航天器软件工程实践出发约定软件缺陷模式描述规范，通过定义如下10元组模型来描述航天器软件缺陷模式属性，具体如表1所示.

表1 航天器软件缺陷模式描述规范Tab.1 Defect pattern specification of spacecraft software

1.3 航天器软件缺陷模式集

根据航天器软件结构化设计模式和所实现的功能需求与非功能性需求(如可靠性和安全性、实时性处理等要求)，对航天器软件缺陷模式进行分类.基于面向对象的思想，抽象出11类航天器软件缺陷模式，如表2所示.

表2 航天器软件缺陷模式类别Tab.2 Defect pattern category of spacecraft software

同时，为了更好地组织软件缺陷模式，从不同粒度表达软件缺陷，本文采用层次化模型描述航天器软件缺陷模式.将软件缺陷模式划分为3层，内容如下：

a) 缺陷模式类别：缺陷模式类别是若干同类缺陷模式的统称，如初始化/复位类、计算/算法类、中断/时序设计类等；

b) 基础缺陷模式：刻画一种相对具体的缺陷形式，如变量声明错误等；

c) 缺陷子模式：是基础缺陷模式的细分，如变量作用域声明错误、局部变量类型声明错误、指针变量类型声明错误均源于变量声明错误的基础缺陷模式.

本文共梳理总结软件基础缺陷模式123项、缺陷子模式170项，形成并建立首个航天器软件缺陷模式集，命名为Spacecraft Software Defect Patterns Set(SSDPS).航天器软件缺陷模式集将实现动态维护，将通过吸收典型案例及常见多发问题实现持续完善.航天器软件缺陷模式集(部分示例)如表3所示.

表3 航天器软件缺陷模式集(计算和算法类)示例Tab.3 Defect Pattern set of spacecraft software

2 缺陷模式自动检测技术研究

2.1 缺陷模式形式化建模

自然语言描述的软件缺陷模式无法在计算机中表达、存储、组织以及自动化使用.为了解决该问题，本文采用模型检测技术中用于描述程序性质的模态/时序逻辑描述语言对软件缺陷模式进行形式化描述，以获取程序性质规约.

航天器软件系统作为典型的并发系统，其运行过程和行为可以抽象为状态转移系统，程序性质则可以通过计算树逻辑(CTL -Computation Tree Logic)进行刻画.计算树逻辑是一种典型的模态/时序逻辑描述语言，可以描述状态的前后关系和分支情况，属于分叉时序逻辑.对于CTL，使用路径量词(包括：A、E)和模态算子(包括：F、G、X、U)对程序性质进行形式化描述[5].其中，量词A(Always)和E(Exists)描述分支情况，分别表示全部计算路径存在和某条计算路径存在；模态算子描述状态的前后关系，如表4所示.

本文以表3中“SSDPS-CALC-005：无符号型整数减操作溢出”为例介绍软件缺陷模式形式化描述过程.

1) 机理分析：根据SSDPS-CALC-005缺陷描述可获知该缺陷产生机理，即：当对一个无符号整数进行算术减操作时，使得其结果取值超过了相应类型的最大值[6].因此，若x、y均为无符号整数，则表达式“x-y”发生无符号型整数减操作溢出缺陷的性质约束条件为“x

2) 形式化语言描述：如果需要判定是否存在无符号型整数减操作溢出，需要对整个程序进行遍历，若某条计算路径中存在表达式满足性质约束条件“x

通过上述方式，可以基于CTL语言对基础缺陷模式“无符号型整数溢出超限”进行如表5所示的形式化描述.

2.2 缺陷模式自动检测技术

软件缺陷模式检测涉及的程序分析技术[7-8]主要包括：直接检索符号表、遍历抽象语法树(AST-Abstract Syntax Tree)进行模式匹配、类型检查、数据流分析、抽象解释、符号执行等.限于篇幅，本文重点对符号执行技术进行说明.

符号执行技术[9]是将系统的原始逻辑转换成符号逻辑，根据符号逻辑来模拟程序执行并得到所有执行状态，分析结果精确，主要用于查找逻辑复杂和发生条件苛刻的软件缺陷.

在符号执行过程中，每当遇到判断与跳转语句时，符号执行分析引擎便会将当前执行路径的路径约束收集到该路径的约束集合中.其中，路径约束(Path Constraint)是指程序分支指令中与输入符号相关的分支条件的取值，是一系列不具有量词的布尔型公式.而路径约束集合则被用来存储每一条程序路径上收集到的约束，用“与”操作进行连接，通过使用约束求解器(Constraint Solver)对约束集合进行求解，可以得到该条路径的可达性：如果约束求解的结果有解，表示该条路径可达，否则表示该条路径不可达.在时间与计算资源足够的理想情况下，符号执行能够遍历目标程序的所有路径并判断其可达性.

本文通过在程序特定状态点处增加性质约束条件，联合路径约束求解实现软件缺陷模式检测，具体流程如图2所示.

图2 基于符号执行的缺陷模式自动检测流程Fig.2 Automatic defect pattern detection process based on symbolic execution

首先，将被分析C程序对象根据抽象语法树(AST)构造控制流图(CFG-Control Flow Graph)，控制流图是编译器内部用有向图表示一个程序过程的一种抽象数据结构，图中的节点表示一个程序基本块，基本块是没有任何跳转的顺序语句代码块，图中的边表示代码中的跳转，它是有向边.在CFG的基础上生成符号执行树，并为每一条路径建立一系列以输入数据为变量的符号表达式.

之后，根据软件缺陷模式需要判定的程序性质添加相应的安全规则和约束.例如，如果要添加缓冲区溢出的安全约束，则在执行时遇到对内存进行操作的语句时，就要对该语句所操作的内存对象的边界添加安全约束.通过上述方式完成软件安全约束的添加.

最后，分析引擎按照控制流程图访问每条语句，并获得程序中每条语句的符号变量及约束信息，并在每次添加安全约束之后使用约束求解器对所有的安全约束进行求解，以判定当前是否可能潜在一个安全问题，即依据求解结果判定是否满足某个缺陷模式对应的程序性质.

本文以无符号型整数减操作导致溢出为例，示例程序及基本检测流程如图3所示.从检测流程可以看出，符号执行会在模拟执行过程中的特定状态点，通过对目标符号进行求解，并与缺陷预期进行比较来暴露出问题.

图3 示例程序片段Fig.3 Program fragment

对程序中使用的变量进行符号表示后，针对无符号型整数减溢出方面的错误可以通过将该缺陷模式的性质约束条件进行求解，如表6所示.

表6 无符号型整数减溢出实例Tab.6 Unsigned integer overflow Instance

检测流程：

1) 检测所有的“-”、“-=”二元运算符.

2) 获取二元运算符的左操作数lhs，右操作数rhs.

3) 如果lhs或rhs都不是污点数据，则获取lhs和rhs的符号值，根据二元操作符，将被减数与减数进行比较，看约束求解的结果就可以检测出无符号型整数是否溢出.在图2的示例中根据我们总结出的程序性质约束条件(S1

2.3 工具设计与实现

本文基于软件缺陷模式自动检测技术的研究，完善了静态分析工具SpecChecker的功能，用于实现典型缺陷模式的自动化检测.图4描述了SpecChecker的体系结构，其主要由预处理、扩展层、配置&调度层、数据层、用户界面组成.在整个框架中，预处理层为公共基础层，为上层所有引擎正常调度执行提供支撑；扩展层主要是为支持更多的缺陷模式类型和分析引擎集成提供接口；配置和调度层主要根据语言、编译平台、编码标准等对引擎进行调度，并通过自定义适配器，将分析结果适配到统一结果模型中；数据层包括了各个分析引擎产生的所有中间数据结果及最终分析结果，结合缺陷类型，为GUI层的结果展示提供数据.

图4 缺陷模式自动检测工具架构Fig.4 The architecture of automated defect pattern detection tools

缺陷模式检测和分析过程主要分两个阶段.

第一阶段，确定被分析源文件及编译器配置，对每个C文件进行预处理，生成预处理后的中间文件；预处理成功后再对每个中间文件进行语法分析，基于中间表示构造器，产生“中间表示”并缓存于分析上下文中，这些“中间表示”主要包括抽象语法树AST、全局符号表、控制流程图CFG、函数调用图等.

第二阶段，“中间表示”生成后，将根据已定义的编码规则或缺陷模式，调用相应的检查器对每个C文件对应的中间表示进行一系列的分析操作，如果发现编码规则违反或典型缺陷模式，将会把缺陷涉及的详细信息(被分析文件、缺陷发生的行号、列号、违反或缺陷提示信息)提交给分析上下文中的错误管理模块.根据编码规则或缺陷模式的定义类型、作用域范围的不同，检查机理和算法也有所差异.

目前，工具已支持116项航天器软件典型缺陷模式的自动检测.其中，部分示例如表7所示.

表7 工具支持自动检测的缺陷模式(示例)Tab.7 Defect patterns that tools support automatic detection

3 实验结果

为验证基于软件缺陷模式的自动检测工具在实际项目中的使用效果，选取某型号四个典型航天嵌入式软件为对象进行实验应用，检测范围为表5中提出的116项航天器软件典型缺陷模式.

1) 上升器PIU软件：处理器为80C32，编译配置为Keil C51，编程语言为C语言，规模(LOC)为4485行，主要完成工程参数的采集、遥控指令的执行、蓄电池安时计电量累计、蓄电池组充电切换功能、蓄电池组过压、过放保护等功能.

2) 微波雷达DSP软件：处理器为SMJ320C6701，编译配置为TI Code Composer Studio2.2，编程语言为C语言，规模(LOC)为3493行，主要完成地检注入数据，完成测距、测速数据处理、校时功能、程序自检功能以及DSP自动监测重配置功能.

3) 中心控制单元应用软件：处理器为TSC695F，编译配置为ERC32(SPARC V7)，编程语言为C语言，规模(LOC)为29401行，实现轨道器各阶段的姿态与轨道控制以及导航和制导任务.

4) CRDS敏感器应用软件：处理器为SOC2008，编译配置为GNU工具包RCC，编程语言为C语言，规模(LOC)为8672行，主要完成目标相对位置和相对姿态角等信息测量.

表8给出了每个被分析软件的实验结果.

表8 被分析项的实验结果Tab.8 The experimental results of the analyzed software

从实验结果中可以看出：

1) 缺陷模式自动检测工具的缺陷检出率超过90%；

2) 工具能够适应于各种编译配置下的软件缺陷模式自动检测；

3) 对于规模较大的软件，如GNC子系统中心控制单元应用软件，工具也能很好的支持.

4 结论与展望

如何更好地了解、掌握航天器软件缺陷产生和发展的规律，控制和减少软件缺陷造成的影响是航天嵌入式软件工程领域致力解决的重要问题.鉴于此，本文通过系统分析和总结航天器软件典型多发问题，建立首个航天器软件缺陷模式集SSDPS；通过时序逻辑语言CTL对软件缺陷模式进行形式化描述，同时开展了以符号执行为代表的缺陷模式自动检测技术研究，完成了缺陷模式自动检测工具SpecChecker的设计与实现.实验结果表明，SpecChecker能够支持大规模软件的问题检测，缺陷检出率超过90%.目前该工具已在空间站、载人航天、深空探测、北斗导航等国家重大航天型号任务的第三方评测中进行了全面应用.

后续课题组将持续完善航天器软件缺陷模式并不断将其固化到缺陷模式自动检测工具中.另一方面，根据航天器软件缺陷模式，进一步研究基于专家系统的软件缺陷预测模型构建技术和基于机器学习的软件缺陷预测模型构建技术，利用人工智能开展软件缺陷的预测和定位.