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

李春光，周曉紅，董龍明

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

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

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

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

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

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

0 引言

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

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

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

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

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

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

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

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

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

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

當(dāng)彈丸質(zhì)量、裝藥批號(hào)、藥溫和火炮藥室長(zhǎng)度等與標(biāo)準(zhǔn)條件不同時(shí)，將會(huì)影響到彈丸的初速.一般情況下初速可表示為：

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

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

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

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

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

以一組簡(jiǎn)單的程序代碼為例，說(shuō)明符號(hào)執(zhí)行算法如何得到測(cè)試用例，使得程序路徑覆蓋率達(dá)到100%。

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

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

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

4 結(jié)論

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

圖3 函數(shù)test的符號(hào)執(zhí)行過(guò)程

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

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

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

［4］許婧祺，董龍明，郝酈波.軍用指揮控制軟件可信性分析與驗(yàn)證技術(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］.計(jì)算機(jī)學(xué)報(bào)，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］.彈道學(xué)報(bào)，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è)計(jì)、計(jì)算機(jī)網(wǎng)絡(luò)。