李春光，周曉紅，董龍明

（1.白城師范學院，吉林 白城 137000；2.長春職業(yè)技術(shù)學院，長春 130033；3.陸軍駐南京地區(qū)軍事代表室，南京 210000）

符號執(zhí)行火控系統(tǒng)諸元解算程序測試用例生成技術(shù)

李春光1，周曉紅2，董龍明3

（1.白城師范學院，吉林 白城 137000；2.長春職業(yè)技術(shù)學院，長春 130033；3.陸軍駐南京地區(qū)軍事代表室，南京 210000）

火控系統(tǒng)作為各種武器裝備的中樞和大腦，控制著武器系統(tǒng)的運轉(zhuǎn)，其有效性直接關(guān)系著射擊的成敗甚至武器系統(tǒng)的綜合效能。諸元解算程序是將各種輸入條件依據(jù)彈道模型經(jīng)過多次迭代轉(zhuǎn)換為射擊諸元，由于其復雜性，當前軟件測試用例只是在幾個關(guān)鍵點上進行校驗，很難覆蓋程序所有分支和路徑，存在著測試不充分。針對這個問題，提出了一種基于符號執(zhí)行的用例自動生成技術(shù)，結(jié)合解彈道方程組約束條件和程序分支控制變量使用符號執(zhí)行框架內(nèi)能夠得到覆蓋所有可能的執(zhí)行路徑，從而保證測試的充分性。

火控系統(tǒng)，諸元解算程序，符號執(zhí)行，測試用例生成技術(shù)

0 引言

隨著武器信息化程度越來越高，使用計算機作為各種武器平臺的中心樞紐：收集和匯總外部和武器平臺各部件數(shù)據(jù)和信息，分析這些數(shù)據(jù)并根據(jù)各種數(shù)學控制模型驅(qū)動各武器部件完成作戰(zhàn)任務(wù)。在自行火炮武器中，火控系統(tǒng)扮演著這樣的角色，完成各類數(shù)據(jù)（目標諸元、氣象諸元、彈道諸元、武器姿態(tài)諸元）的處理計算任務(wù)，根據(jù)彈道方程或射表數(shù)學模型計算射擊諸元并轉(zhuǎn)換完各類控制信號驅(qū)動火控系統(tǒng)的掉炮和射擊。與傳統(tǒng)火炮射擊相比，現(xiàn)代火控系統(tǒng)諸元解算程序一般采用射表數(shù)據(jù)擬合和解外彈道方程相結(jié)合的方法，對彈道系統(tǒng)、表尺等數(shù)據(jù)進行擬合，然后解彈道方程組逐步迭代求得射擊諸元［1］。

迭代過程在程序中通常情況是由while或for循環(huán)語句實現(xiàn)的，循環(huán)控制語句一般由迭代次數(shù)或精度約束條件來控制，迭代的次數(shù)越多得到的射擊諸元越精確，但消耗的時間和計算機內(nèi)存越大。這類程序的正確性保證一般使用軟件測試技術(shù)［2］來保證：針對已知射表數(shù)據(jù)值，運行程序，比較其執(zhí)行結(jié)果與已經(jīng)值判斷程序中是否有錯。但是，該方法不能保證諸元解算程序沒有錯誤，尤其是針對邊界條件或特殊分支路徑執(zhí)行很難進行測試。而在火炮一次射擊任務(wù)中，某個諸元求解錯誤（比如：浮點數(shù)值越界或除零錯等）導致諸元求解得到的數(shù)據(jù)超出預(yù)估，導致整個射擊任務(wù)失敗甚至人員傷亡。與動態(tài)的測試方法不同，靜態(tài)分析技術(shù)［3-4］在不運行程序情況下根據(jù)程序的語義對程序進行抽象檢查直接分析程序代碼，發(fā)現(xiàn)其中一些錯誤，典型的應(yīng)用例如：C語言指針分析［5］、變量值范圍分析［6］。相比而言，靜態(tài)分析技術(shù)具有自動化程度高、覆蓋率高以及易于擴展等優(yōu)點。本文在符號執(zhí)行技術(shù)框架內(nèi)，將火控系統(tǒng)諸元解算方程數(shù)據(jù)模型作為符執(zhí)行約束求解器，計算得到一組能否覆蓋諸元解算程序所有分支的輸入數(shù)據(jù)，用于火控系統(tǒng)諸元解算程序測試用例，能夠保證測試的充分性，并取得比較高的路徑覆蓋率。

1 符號執(zhí)行技術(shù)

符號執(zhí)行技術(shù)首先由King在1976年提出［7］，經(jīng)過30多年發(fā)展，其理論和技術(shù)不斷完善，已被廣泛地應(yīng)用于理論研究和工程實踐。其主要思想是指在不執(zhí)行程序的前提下，用符號作為值賦給變量，對程序的執(zhí)行路徑進行模擬執(zhí)行，并進行相關(guān)分析的技術(shù)。它能很精確地分析程序的代碼屬性，分析精度高。通過符號執(zhí)行可以得到一組關(guān)于變量初始值的約束——稱為路徑條件，給定的程序路徑是可行的，當且僅當路徑是可被滿足的。

基于符號執(zhí)行技術(shù)的程序源代碼分析框架如圖1所示。首先，利用開源編譯器前端將待分析的軟件成品功能模塊源程序解析成各種計算機可存儲和理解的中間形式，如：抽象語法樹、符號表、函數(shù)調(diào)用圖、控制流圖、等形式。其中，控制流圖（CFG）是用有向圖表示一個程序過程控制結(jié)構(gòu)的抽象數(shù)據(jù)結(jié)構(gòu)，圖中的節(jié)點表示一個程序基本塊，邊表示代碼中的跳轉(zhuǎn)。符號調(diào)度器是基于每種特定程序符號值的操作語義在控制流圖邊指向上依次模擬調(diào)度執(zhí)行每條語句，在遇到分支節(jié)點時，使用約束求解器判定哪條分支可行，并得到一組該可執(zhí)行路徑的關(guān)于程序變量的解。當所有控制流圖上所有節(jié)點和邊遍歷結(jié)束時，就能得到覆蓋所有可執(zhí)行路徑的一組關(guān)于程序變量的數(shù)據(jù)。

圖1 符號執(zhí)行框架

在符號執(zhí)行框架中，有兩種技術(shù)影響符號執(zhí)行框架的效率：①符號調(diào)度器。通?；谟邢驁D搜索策略的不同可以分為：深度遍歷和寬度遍歷。當前，符號調(diào)度器比較有名的研究性成果有EXE、JPF-SE、KLEE等。②約束求解器。是獲取滿足一組約束的解，典型代表性工作有SAT/SMT求解器。隨著約束求解技術(shù)飛速發(fā)展，已經(jīng)能夠解決實際領(lǐng)域中許多問題，例如：符號執(zhí)行工具KLEE調(diào)用STP約束求解器求解所有路徑的約束條件真值；Z3已成功應(yīng)用于微軟項目Spec#/Boogie中。

2 基于解彈道方程組的約束求解器

作為現(xiàn)代火炮系統(tǒng)的核心任務(wù)之一，諸元解算一般采用數(shù)值方法解彈道方程的方法計算射擊參數(shù)，并使用計算機程序循環(huán)通過多次迭代接近最佳解，通過控制精度約束條件得到滿足一定精度的射擊諸元。解彈道方程方法一般分為兩種：一是將彈丸作為剛體彈道模型，另一種是將彈丸作為質(zhì)點彈道模型。本文以后一種為例，非標準條件下彈丸質(zhì)心運動微分方程組［7］如下：

初 始 條 件 為 t=0 時 ，x0=0，y0=Hp，z0=0，vx0=v0cosθ0，vy0=v0sinθ0，vz0=0。彈道條件是指初速、藥溫、裝藥質(zhì)量、彈丸質(zhì)量。

當彈丸質(zhì)量、裝藥批號、藥溫和火炮藥室長度等與標準條件不同時，將會影響到彈丸的初速.一般情況下初速可表示為：

式中，v0為火炮射擊時彈丸的實際初速，v0n為火炮的喪定初速（即標準初速），Δv0m為彈丸質(zhì)量引起的初速改變量，Δv0y為裝藥批號不同引起的初速偏差，Δv0ty為藥溫非標準引起的初速改變量；Δv0p為火炮初速減退量。

利用彈道方程求解射擊諸元時，還需要考慮氣象諸元，將氣象觀察系統(tǒng)探測得到的真實氣象諸元以一定形式（如計算機氣象通報）采用點點插值或擬合成曲線代入到方程。火控計算機使用軟件基于迭代算法逐步求解逼近最佳射擊參數(shù)時，基于上述原理可到看到針對不同的初始輸入數(shù)據(jù)，這些彈道條件和氣象條件影響程序運行路徑（包括選擇分支和循環(huán)迭代次數(shù)）。在圖1符號執(zhí)行框架下，基于彈丸質(zhì)心運動微分方程組設(shè)計約束求解器SolverBTA，用來求解某條可執(zhí)行路徑上的一組約束，最終得到一組包括炮目位置、射擊條件、氣象條件等最小初始輸入數(shù)據(jù)集，使得覆蓋率達到100%，通過運行這組輸入數(shù)據(jù)得到相應(yīng)一組射擊諸元，判斷這組射擊諸元的正確性評判火控軟件在各種環(huán)境下程序是否發(fā)生改變。

3 基于約束求解符號執(zhí)行算法框架

本節(jié)以偽代碼形式描述基于約束求解符號執(zhí)行算法框架，得到每個可達的程序點關(guān)于變量的符號值，迭代過程使用隊列存儲結(jié)果，主要操作包括：從隊列的首部彈出數(shù)據(jù)項pop操作和將數(shù)據(jù)項存入隊列首部push操作。W存儲符號執(zhí)行計算的語句及變量的符號值。該算法偽代碼描述如下：

公式［［s］］表示基于符號值的程序操作語義，公式Succ（s）表示語句s在控制流圖上的后繼。在循環(huán)控制條件語句處，調(diào)用約束求解器SolverBTA判斷條件的真值與否，如果多個分支路徑都是可能的，則逐個執(zhí)行每個分支。

以一組簡單的程序代碼為例，說明符號執(zhí)行算法如何得到測試用例，使得程序路徑覆蓋率達到100%。

可以構(gòu)建代碼函數(shù)test的控制流圖CFG，只包含了2條路徑，如圖2所示?；诩s束求解符號執(zhí)行框架的分析過程如下頁圖3所示，以符號值為輸入，模擬執(zhí)行代碼，遇到分支語句時，使用約束求解判定路徑的可行性。

圖2 函數(shù)test的控制流圖

本示例使用的是“深度優(yōu)先”的路徑調(diào)度策略，使用約束求解器可以求解出分別觸發(fā)這兩條路徑的兩個測試例輸入及對應(yīng)的返回值。對程序變量i一組賦值集{9，11}，可以覆蓋函數(shù)test兩個分支路徑。通過這個示例可以看出，使用基于約束求解的符號執(zhí)行方法對程序源代碼進行分析，可以覆蓋所有分支執(zhí)行路徑，用來檢驗火控系統(tǒng)諸元解算程序在各種復雜輸入條件下的分支執(zhí)行。

4 結(jié)論

為保證火控系統(tǒng)諸元解算程序測試的充分性，提出一種基于符號執(zhí)行的火控系統(tǒng)諸元解算程序測試用例自動生成技術(shù)。該技術(shù)將解彈道方程組作為符號執(zhí)行框架的約束求解器，指導符號調(diào)度器得到能覆蓋所有分支的一組輸入數(shù)據(jù)，實例表明該技術(shù)的有效性。

圖3 函數(shù)test的符號執(zhí)行過程

［1］劉怡析，劉玉文.外彈道學［M］.北京：海潮出版社，1999.

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

［3］張健.精確的程序靜態(tài)分析［J］.計算機學報，2008，31（9）：1549-1553.

［4］許婧祺，董龍明，郝酈波.軍用指揮控制軟件可信性分析與驗證技術(shù) ［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］陳立前，王戟，侯蘇寧.單變量區(qū)間線性不等式抽象域［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- ），男，吉林洮南人，碩士，講師。研究方向：嵌入式程序設(shè)計、計算機網(wǎng)絡(luò)。