符号执行火控系统诸元解算程序测试用例生成技术

李春光，周晓红，董龙明

（1.白城师范学院，吉林 白城 137000；2.长春职业技术学院，长春 130033；3.陆军驻南京地区军事代表室，南京 210000）

符号执行火控系统诸元解算程序测试用例生成技术

李春光1，周晓红2，董龙明3

（1.白城师范学院，吉林 白城 137000；2.长春职业技术学院，长春 130033；3.陆军驻南京地区军事代表室，南京 210000）

火控系统作为各种武器装备的中枢和大脑，控制着武器系统的运转，其有效性直接关系着射击的成败甚至武器系统的综合效能。诸元解算程序是将各种输入条件依据弹道模型经过多次迭代转换为射击诸元，由于其复杂性，当前软件测试用例只是在几个关键点上进行校验，很难覆盖程序所有分支和路径，存在着测试不充分。针对这个问题，提出了一种基于符号执行的用例自动生成技术，结合解弹道方程组约束条件和程序分支控制变量使用符号执行框架内能够得到覆盖所有可能的执行路径，从而保证测试的充分性。

火控系统，诸元解算程序，符号执行，测试用例生成技术

0 引言

随着武器信息化程度越来越高，使用计算机作为各种武器平台的中心枢纽：收集和汇总外部和武器平台各部件数据和信息，分析这些数据并根据各种数学控制模型驱动各武器部件完成作战任务。在自行火炮武器中，火控系统扮演着这样的角色，完成各类数据（目标诸元、气象诸元、弹道诸元、武器姿态诸元）的处理计算任务，根据弹道方程或射表数学模型计算射击诸元并转换完各类控制信号驱动火控系统的掉炮和射击。与传统火炮射击相比，现代火控系统诸元解算程序一般采用射表数据拟合和解外弹道方程相结合的方法，对弹道系统、表尺等数据进行拟合，然后解弹道方程组逐步迭代求得射击诸元［1］。

迭代过程在程序中通常情况是由while或for循环语句实现的，循环控制语句一般由迭代次数或精度约束条件来控制，迭代的次数越多得到的射击诸元越精确，但消耗的时间和计算机内存越大。这类程序的正确性保证一般使用软件测试技术［2］来保证：针对已知射表数据值，运行程序，比较其执行结果与已经值判断程序中是否有错。但是，该方法不能保证诸元解算程序没有错误，尤其是针对边界条件或特殊分支路径执行很难进行测试。而在火炮一次射击任务中，某个诸元求解错误（比如：浮点数值越界或除零错等）导致诸元求解得到的数据超出预估，导致整个射击任务失败甚至人员伤亡。与动态的测试方法不同，静态分析技术［3-4］在不运行程序情况下根据程序的语义对程序进行抽象检查直接分析程序代码，发现其中一些错误，典型的应用例如：C语言指针分析［5］、变量值范围分析［6］。相比而言，静态分析技术具有自动化程度高、覆盖率高以及易于扩展等优点。本文在符号执行技术框架内，将火控系统诸元解算方程数据模型作为符执行约束求解器，计算得到一组能否覆盖诸元解算程序所有分支的输入数据，用于火控系统诸元解算程序测试用例，能够保证测试的充分性，并取得比较高的路径覆盖率。

1 符号执行技术

符号执行技术首先由King在1976年提出［7］，经过30多年发展，其理论和技术不断完善，已被广泛地应用于理论研究和工程实践。其主要思想是指在不执行程序的前提下，用符号作为值赋给变量，对程序的执行路径进行模拟执行，并进行相关分析的技术。它能很精确地分析程序的代码属性，分析精度高。通过符号执行可以得到一组关于变量初始值的约束——称为路径条件，给定的程序路径是可行的，当且仅当路径是可被满足的。

基于符号执行技术的程序源代码分析框架如图1所示。首先，利用开源编译器前端将待分析的软件成品功能模块源程序解析成各种计算机可存储和理解的中间形式，如：抽象语法树、符号表、函数调用图、控制流图、等形式。其中，控制流图（CFG）是用有向图表示一个程序过程控制结构的抽象数据结构，图中的节点表示一个程序基本块，边表示代码中的跳转。符号调度器是基于每种特定程序符号值的操作语义在控制流图边指向上依次模拟调度执行每条语句，在遇到分支节点时，使用约束求解器判定哪条分支可行，并得到一组该可执行路径的关于程序变量的解。当所有控制流图上所有节点和边遍历结束时，就能得到覆盖所有可执行路径的一组关于程序变量的数据。

图1 符号执行框架

在符号执行框架中，有两种技术影响符号执行框架的效率：①符号调度器。通常基于有向图搜索策略的不同可以分为：深度遍历和宽度遍历。当前，符号调度器比较有名的研究性成果有EXE、JPF-SE、KLEE等。②约束求解器。是获取满足一组约束的解，典型代表性工作有SAT/SMT求解器。随着约束求解技术飞速发展，已经能够解决实际领域中许多问题，例如：符号执行工具KLEE调用STP约束求解器求解所有路径的约束条件真值；Z3已成功应用于微软项目Spec#/Boogie中。

2 基于解弹道方程组的约束求解器

作为现代火炮系统的核心任务之一，诸元解算一般采用数值方法解弹道方程的方法计算射击参数，并使用计算机程序循环通过多次迭代接近最佳解，通过控制精度约束条件得到满足一定精度的射击诸元。解弹道方程方法一般分为两种：一是将弹丸作为刚体弹道模型，另一种是将弹丸作为质点弹道模型。本文以后一种为例，非标准条件下弹丸质心运动微分方程组［7］如下：

初 始 条 件 为 t=0 时 ，x0=0，y0=Hp，z0=0，vx0=v0cosθ0，vy0=v0sinθ0，vz0=0。弹道条件是指初速、药温、装药质量、弹丸质量。

当弹丸质量、装药批号、药温和火炮药室长度等与标准条件不同时，将会影响到弹丸的初速.一般情况下初速可表示为：

式中，v0为火炮射击时弹丸的实际初速，v0n为火炮的丧定初速（即标准初速），Δv0m为弹丸质量引起的初速改变量，Δv0y为装药批号不同引起的初速偏差，Δv0ty为药温非标准引起的初速改变量；Δv0p为火炮初速减退量。

利用弹道方程求解射击诸元时，还需要考虑气象诸元，将气象观察系统探测得到的真实气象诸元以一定形式（如计算机气象通报）采用点点插值或拟合成曲线代入到方程。火控计算机使用软件基于迭代算法逐步求解逼近最佳射击参数时，基于上述原理可到看到针对不同的初始输入数据，这些弹道条件和气象条件影响程序运行路径（包括选择分支和循环迭代次数）。在图1符号执行框架下，基于弹丸质心运动微分方程组设计约束求解器SolverBTA，用来求解某条可执行路径上的一组约束，最终得到一组包括炮目位置、射击条件、气象条件等最小初始输入数据集，使得覆盖率达到100%，通过运行这组输入数据得到相应一组射击诸元，判断这组射击诸元的正确性评判火控软件在各种环境下程序是否发生改变。

3 基于约束求解符号执行算法框架

本节以伪代码形式描述基于约束求解符号执行算法框架，得到每个可达的程序点关于变量的符号值，迭代过程使用队列存储结果，主要操作包括：从队列的首部弹出数据项pop操作和将数据项存入队列首部push操作。W存储符号执行计算的语句及变量的符号值。该算法伪代码描述如下：

公式［［s］］表示基于符号值的程序操作语义，公式Succ（s）表示语句s在控制流图上的后继。在循环控制条件语句处，调用约束求解器SolverBTA判断条件的真值与否，如果多个分支路径都是可能的，则逐个执行每个分支。

以一组简单的程序代码为例，说明符号执行算法如何得到测试用例，使得程序路径覆盖率达到100%。

可以构建代码函数test的控制流图CFG，只包含了2条路径，如图2所示。基于约束求解符号执行框架的分析过程如下页图3所示，以符号值为输入，模拟执行代码，遇到分支语句时，使用约束求解判定路径的可行性。

图2 函数test的控制流图

本示例使用的是“深度优先”的路径调度策略，使用约束求解器可以求解出分别触发这两条路径的两个测试例输入及对应的返回值。对程序变量i一组赋值集{9，11}，可以覆盖函数test两个分支路径。通过这个示例可以看出，使用基于约束求解的符号执行方法对程序源代码进行分析，可以覆盖所有分支执行路径，用来检验火控系统诸元解算程序在各种复杂输入条件下的分支执行。

4 结论

为保证火控系统诸元解算程序测试的充分性，提出一种基于符号执行的火控系统诸元解算程序测试用例自动生成技术。该技术将解弹道方程组作为符号执行框架的约束求解器，指导符号调度器得到能覆盖所有分支的一组输入数据，实例表明该技术的有效性。

图3 函数test的符号执行过程

［1］刘怡析，刘玉文.外弹道学［M］.北京：海潮出版社，1999.

［2］MYERS G J，SANDLER C.The art of software testing［M］.Jersey：John Wiley&Sons，2004.

［3］张健.精确的程序静态分析［J］.计算机学报，2008，31（9）：1549-1553.

［4］许婧祺，董龙明，郝郦波.军用指挥控制软件可信性分析与验证技术 ［J］.火力与指挥控制，2015，40（8）：176-180.

［5］HORWITZ S.Precise flow-insensitive may-alias is NP-hard［J］.ACM Transactions on Programming Languages and Systems，1997，19（1）：1-6.

［6］陈立前，王戟，侯苏宁.单变量区间线性不等式抽象域［J］.计算机学报，2010，33（3）：427-439.

［7］ KING J C.Symbolic execution and program testing［J］.Communications of the ACM，1976，19（7）：385-394.

［8］陈春，刘玉文.弹道积分法决定射击诸元的建模及精度分析［J］.弹道学报，2001，13（1）：17-21.

A Symbolic Execution Based Test Case Generation for Data-calculation Programs of Fire Control System

LI Chun-guang1，ZHOU Xiao-hong2，DONG Long-ming3
（1.Baicheng Normal University，Baicheng 137000，China；2.Changchun Vocational Institute of Technology，Changchun 130033，China；3.Nanjing Military Representative Office of PLA Army，Nanjing 210000，China）

The fire control system，as the center and the brain of various weapons，controls the operation of the weapon system.Its effectiveness is directly related to the success of the fire and even the comprehensive effectiveness of the weapon system.Data-calculation programs transform a variety of input conditions into the firing data after several iterations according to the trajectory model.Because of its complexity，current software testing technology can verify only on several key points，which is difficult to cover all branches and paths of the programs and is insufficient.To solve this problem，an automatic generation of testing use case based on symbolic execution is proposed.The constraints of the solution trajectory equations and the program control branches are used to obtain all possible execution paths within the framework of symbol execution.This method is sure of the adequate testing.

fire control system，data-calculation programs，symbolic execution，test case generation

TP39；TJ81+0.376

A

10.3969/j.issn.1002-0640.2017.07.034

1002-0640（2017）07-0157-04

2016-05-11

2016-06-27

李春光（1980- ），男，吉林洮南人，硕士，讲师。研究方向：嵌入式程序设计、计算机网络。