許婧祺，董龍明，郝麗波

（1.湖南機(jī)電職業(yè)技術(shù)學(xué)院，長(zhǎng)沙410073；2.總裝備部駐南京地區(qū)軍事代表室，南京210000）

軍用指揮控制軟件可信性分析與驗(yàn)證技術(shù)*

許婧祺1，董龍明2，郝麗波1

（1.湖南機(jī)電職業(yè)技術(shù)學(xué)院，長(zhǎng)沙410073；2.總裝備部駐南京地區(qū)軍事代表室，南京210000）

隨著武器裝備信息化程度越來(lái)越高，軍用指揮控制軟件的可信性直接關(guān)系到裝備整體效能的發(fā)揮。在對(duì)傳統(tǒng)軟件質(zhì)量保證技術(shù)研究的基礎(chǔ)上，結(jié)合軍用指揮控制軟件的特點(diǎn)，提出了基于形式化方法的軟件分析與驗(yàn)證技術(shù)。分別從安全性質(zhì)形式化規(guī)約技術(shù)、基于模型檢驗(yàn)的指揮軟件驗(yàn)證技術(shù)和基于靜態(tài)分析的控制軟件分析技術(shù)三方面保證軍用指揮控制軟件的可信性，最后，提出了適用于指揮控制軟件全生命周期開(kāi)發(fā)的形式化分析與驗(yàn)證集成環(huán)境。

軍用指揮控制軟件，分析與驗(yàn)證技術(shù)，模型檢驗(yàn)，靜態(tài)分析

0　引言

隨著新軍事變革的深入，武器裝備的信息化、智能化程度越來(lái)越高，軟件在整個(gè)武器系統(tǒng)中扮演的角色越來(lái)越重要，例如：數(shù)值計(jì)算、信息處理、智能決策、行為控制等，無(wú)不存在著軟件的身影。在高技術(shù)戰(zhàn)爭(zhēng)過(guò)程中，軟件起著無(wú)可替代的作用，大至戰(zhàn)役規(guī)劃、戰(zhàn)場(chǎng)決策，小到諸元標(biāo)定、指令下達(dá)、武器裝備單元控制等。在體系作戰(zhàn)中，軟件產(chǎn)品負(fù)責(zé)信息收集、加工、處理、儲(chǔ)存、分發(fā)等任務(wù)，將各個(gè)獨(dú)立的武器裝備互聯(lián)互通成一個(gè)有機(jī)的整體。軟件的復(fù)雜性也將會(huì)進(jìn)一步增加，對(duì)軟件功能和安全性的要求也會(huì)越來(lái)越高，其正確性和可信性直接關(guān)系到武器系統(tǒng)的有效性，甚至直接關(guān)系到戰(zhàn)爭(zhēng)的勝負(fù)。一方面，我們感受著軟件帶來(lái)的好處，同樣的武器硬件平臺(tái)，由于軟件的改進(jìn)，武器系統(tǒng)反應(yīng)時(shí)間、打擊的精度和殺傷力大幅提高；另外一方面，隨著武器系統(tǒng)功能越來(lái)越復(fù)雜，軟件規(guī)模越來(lái)越大，軟件質(zhì)量難以得到保證。武器系統(tǒng)中某個(gè)軟件模塊的缺陷或錯(cuò)誤可能導(dǎo)致整個(gè)武器系統(tǒng)的失效，甚至導(dǎo)致重大經(jīng)濟(jì)損失和人員的傷亡。例如：1996年，歐洲空間局的阿麗亞娜火箭發(fā)射37 s后爆炸導(dǎo)致6億美元的損失是由于在一個(gè)64位浮點(diǎn)整數(shù)轉(zhuǎn)換為16位有符號(hào)整數(shù)時(shí)產(chǎn)生溢出。美國(guó)國(guó)家標(biāo)準(zhǔn)技術(shù)研究所發(fā)布報(bào)告，2002年美國(guó)由于軟件缺陷而引起的損失額高達(dá)592億美元，占美國(guó)國(guó)內(nèi)生產(chǎn)總值的0.6%。因此，總裝備部為了提高軍用軟件質(zhì)量，制定了國(guó)軍標(biāo)GJB 4072A-2006《軍用軟件質(zhì)量監(jiān)督要求》［1］，規(guī)定了軍用軟件研制整個(gè)過(guò)程的質(zhì)量監(jiān)督的依據(jù)、目的、原則和要求，明確軟件質(zhì)量監(jiān)督全過(guò)程管理的規(guī)范，但是沒(méi)有說(shuō)明在軟件研制各個(gè)過(guò)程中可以使用的軟件質(zhì)量保證技術(shù)。軟件安全性（Safety）［2］是指在規(guī)定的條件下、規(guī)定的時(shí)間內(nèi)，軟件運(yùn)行不引起任務(wù)失敗、人員傷亡、造成重大政治影響或者經(jīng)濟(jì)損失等系統(tǒng)事故的能力。本文針對(duì)陸軍指揮控制軟件的機(jī)理及安全性要求，在分析傳統(tǒng)軟件質(zhì)量保證技術(shù)不足的基礎(chǔ)上，提出軟件可信性保證形式化分析與驗(yàn)證技術(shù)。

1　傳統(tǒng)軟件質(zhì)量保證技術(shù)

1.1軍用軟件成熟度模型

軟件能力成熟度模型（Capability Maturity Model for Software，CMM）［3-4］是對(duì)軟件組織在定義、實(shí)現(xiàn)、度量、控制和改善其軟件過(guò)程的進(jìn)程中各個(gè)發(fā)展階段的描述，本質(zhì)是通過(guò)履行一系列的關(guān)鍵過(guò)程域中關(guān)鍵實(shí)踐來(lái)達(dá)到軟件過(guò)程的目的。CMM可以分為5個(gè)等級(jí)：

（1）初始級(jí)。它的軟件過(guò)程管理處于無(wú)序的、混亂的狀態(tài)，軟件項(xiàng)目的成功完全依賴于個(gè)人能力和團(tuán)隊(duì)的合作，軟件的進(jìn)度、質(zhì)量、預(yù)算均不可測(cè)。

（2）可重復(fù)級(jí)。它的主要特征是已經(jīng)建立了管理軟件項(xiàng)目的方針和實(shí)施這些方針的規(guī)程。軟件組織要對(duì)正在實(shí)施的和已經(jīng)實(shí)施的軟件項(xiàng)目進(jìn)行經(jīng)驗(yàn)總結(jié)，從而抽象出軟件過(guò)程實(shí)施當(dāng)中有效的、具體的、適用的方法，并將其文檔化，形成規(guī)程，為以后的項(xiàng)目預(yù)算、評(píng)估和軟件過(guò)程實(shí)施提供依據(jù)。通過(guò)執(zhí)行已文檔化的規(guī)程，對(duì)當(dāng)前項(xiàng)目形成有效的控制，產(chǎn)生穩(wěn)定的軟件過(guò)程能力。

（3）已定義級(jí)。它的主要特征是標(biāo)準(zhǔn)化。已定義級(jí)與可重復(fù)級(jí)相比，更強(qiáng)調(diào)軟件開(kāi)發(fā)各有關(guān)組織的相互協(xié)調(diào)和作為一個(gè)統(tǒng)一的整體參與軟件的開(kāi)發(fā)。在這一等級(jí)上，組織開(kāi)發(fā)和維護(hù)軟件的過(guò)程已經(jīng)文檔化，軟件工程過(guò)程和軟件管理過(guò)程被綜合為一個(gè)有機(jī)的整體，稱為標(biāo)準(zhǔn)軟件過(guò)程。通過(guò)剪裁標(biāo)準(zhǔn)化軟件過(guò)程和適當(dāng)?shù)匦薷?，產(chǎn)生文檔化的項(xiàng)目的軟件過(guò)程。這樣每一個(gè)項(xiàng)目軟件過(guò)程都是從標(biāo)準(zhǔn)軟件過(guò)程發(fā)展而來(lái)，它們是穩(wěn)定的、可重復(fù)的，成本、進(jìn)度及軟件質(zhì)量處于一定的受控狀態(tài)。

（4）已管理級(jí)。它的特征是定量化。組織對(duì)軟件產(chǎn)品和過(guò)程設(shè)置定量的質(zhì)量目標(biāo)，并限定這些目標(biāo)的變化范圍。整個(gè)等級(jí)的軟件過(guò)程有妥善的定義和一致的度量尺度，組織的軟件過(guò)程能力可以預(yù)測(cè)，對(duì)于新領(lǐng)域的軟件過(guò)程控制，軟件成熟度模型CMM描述項(xiàng)目開(kāi)發(fā)工作也可以評(píng)測(cè)其風(fēng)險(xiǎn)。

（5）優(yōu)化級(jí)。它的特征是對(duì)軟件過(guò)程的不斷改進(jìn)，從而使軟件過(guò)程能力不斷提高，軟件缺陷得到預(yù)防。通過(guò)對(duì)以往的軟件過(guò)程分析，鑒別各種技術(shù)革新，并選擇最優(yōu)的進(jìn)行推廣。

1.2軟件測(cè)試技術(shù)

軟件測(cè)試是軟件開(kāi)發(fā)過(guò)程中十分重要的步驟，是保證軟件功能正確的重要過(guò)程。根據(jù)軟件開(kāi)發(fā)周期階段進(jìn)行劃分，軟件測(cè)試一般可以劃分為單元測(cè)試、集成測(cè)試、系統(tǒng)測(cè)試、驗(yàn)收測(cè)試和回歸測(cè)試。根據(jù)測(cè)試用例（也稱為測(cè)試數(shù)據(jù)）的選擇或產(chǎn)生方法不同，動(dòng)態(tài)測(cè)試又可以分為基于規(guī)范的測(cè)試（又稱為黑盒測(cè)試或功能測(cè)試）、基于程序的測(cè)試（又稱為白盒測(cè)試或結(jié)構(gòu)測(cè)試）以及規(guī)范與程序的聯(lián)合測(cè)試?；谝?guī)范的測(cè)試指根據(jù)軟件規(guī)范或軟件輸入輸出關(guān)系產(chǎn)生測(cè)試用例，并判斷測(cè)試結(jié)果的正確性（也稱為進(jìn)行測(cè)試失效辨識(shí)）；基于程序的測(cè)試則需要根據(jù)程序的內(nèi)部結(jié)構(gòu)特征和與執(zhí)行路徑相關(guān)的數(shù)據(jù)特征產(chǎn)生測(cè)試用例。除了基本的功能性測(cè)試外，還要考慮對(duì)軟件的許多非功能性需求進(jìn)行測(cè)試，包括性能測(cè)試、兼容性測(cè)試、用戶界面測(cè)試、多語(yǔ)言測(cè)試、安全性測(cè)試、可靠性測(cè)試、安裝測(cè)試等等。

2　基于形式化方法的指揮控制軟件分析與驗(yàn)證技術(shù)

軟件成熟度模型是通過(guò)第三方從軟件工程領(lǐng)域規(guī)范軟件開(kāi)發(fā)人員的行為和流程；軟件測(cè)試技術(shù)是設(shè)計(jì)測(cè)試案例驗(yàn)證軟件產(chǎn)品滿足用戶需求、實(shí)現(xiàn)合同中的功能，是一種標(biāo)準(zhǔn)化流程標(biāo)準(zhǔn)，從軟件開(kāi)發(fā)流程規(guī)范軟件開(kāi)發(fā)人員的行為，從規(guī)章制度上杜絕軟件開(kāi)發(fā)過(guò)程中可能的出錯(cuò)。軟件測(cè)試技術(shù)自動(dòng)化程度比較高，有許多成熟的自動(dòng)化方法和工具，是當(dāng)前工業(yè)界常采用的方法，但是受限于測(cè)試案例的設(shè)計(jì)和覆蓋率，不能完全保證該軟件沒(méi)有缺陷和錯(cuò)誤軟件。形式化分析與驗(yàn)證方法能夠完全證明軟件在任何條件下沒(méi)有錯(cuò)誤，但是對(duì)軟件質(zhì)量保證人員要求比較高，需要比較深的數(shù)學(xué)和邏輯功底，能夠建立軟件各種規(guī)范化模型和邏輯推理能力，是當(dāng)前學(xué)術(shù)界研究比較多的方法。

2.1安全性質(zhì)形式化規(guī)約技術(shù)

對(duì)軟件進(jìn)行形式化驗(yàn)證的主要目的就是驗(yàn)證軟件是否滿足某些目標(biāo)性質(zhì)。這些目標(biāo)性質(zhì)分為安全性（Safety）和活性（Liveness）兩大類，安全性是指軟件在運(yùn)行過(guò)程中不發(fā)生非預(yù)期的行為，如運(yùn)行時(shí)不發(fā)生崩潰等；活性是指預(yù)期的行為在軟件的運(yùn)行過(guò)程中總會(huì)發(fā)生，如程序的終止性等。

在指揮控制軟件的實(shí)際開(kāi)發(fā)與應(yīng)用中，用戶往往在軟件的功能和行為級(jí)描述所需的安全性質(zhì)。為了能夠分析和驗(yàn)證軟件是否滿足這些性質(zhì)，首先需要研究如何將用戶的頂層需求模型轉(zhuǎn)換和映射為等價(jià)的、源代碼級(jí)可體現(xiàn)的性質(zhì)。例如，“軟件運(yùn)行時(shí)不會(huì)崩潰”這一安全性質(zhì)映射到源代碼級(jí)實(shí)際上包括無(wú)算術(shù)溢出、無(wú)除零錯(cuò)、無(wú)數(shù)組越界、無(wú)空指針引用等性質(zhì)。將安全性質(zhì)映射到軟件源代碼層面以后，還需要研究如何采用精確、嚴(yán)格的方式對(duì)其進(jìn)行形式化規(guī)約，為形式化分析和驗(yàn)證過(guò)程提供目標(biāo)。

軍用指揮控制軟件涉及到兩類安全性質(zhì)，一類是模型級(jí)時(shí)序性質(zhì)，一類是源代碼級(jí)的運(yùn)行時(shí)錯(cuò)誤。時(shí)序性質(zhì)主要指指揮軟件中用戶對(duì)某些操作的序列有所規(guī)定。時(shí)序性質(zhì)對(duì)于刻畫(huà)指揮軟件中的常見(jiàn)反應(yīng)式性質(zhì)，比如“p操作發(fā)生后q操作一定將會(huì)發(fā)生”。時(shí)序性質(zhì)適合于描述關(guān)于并發(fā)的一些性質(zhì)，比如沒(méi)有死鎖。源代碼級(jí)的運(yùn)行時(shí)錯(cuò)誤指武器控制程序在運(yùn)行過(guò)程中可能發(fā)生的錯(cuò)誤，武器控制軟件中的運(yùn)行時(shí)錯(cuò)誤一般包括：算術(shù)溢出、數(shù)組訪問(wèn)越界、無(wú)效算術(shù)操作（除零錯(cuò)、對(duì)負(fù)數(shù)開(kāi)平方根等）、訪問(wèn)未初始化變量、空指針引用等。

軍用指揮控制軟件安全性質(zhì)形式化規(guī)約方法有3種：第1種是基于可達(dá)性（Reachability）的性質(zhì)規(guī)約描述方法；第2種是基于自動(dòng)機(jī)的性質(zhì)規(guī)約描述方法；第3種是基于時(shí)序邏輯的性質(zhì)規(guī)約描述方法。這3種性質(zhì)規(guī)約方法具有不同的特點(diǎn)，適合不同的應(yīng)用?；诳蛇_(dá)性的性質(zhì)規(guī)約描述方法最為簡(jiǎn)單，它描述的是軟件源代碼中某個(gè)程序點(diǎn)（比如某個(gè)判斷用戶指定性質(zhì)出錯(cuò)的位置）在軟件的運(yùn)行過(guò)程中可達(dá)或不可達(dá)，但其描述能力較弱不適合描述復(fù)雜的時(shí)序性質(zhì)?；谧詣?dòng)機(jī)的規(guī)約描述方法的描述能力是足夠強(qiáng)的，它可以描述軟件的時(shí)序和并發(fā)性質(zhì)，而且表示直觀、處理方便，因此，得到了廣泛的應(yīng)用，如有窮自動(dòng)機(jī)、下推自動(dòng)機(jī)等?；跁r(shí)序邏輯的規(guī)約描述方法的描述能力也較強(qiáng)，表示形式也比較簡(jiǎn)潔直觀，但一般情況下描述能力弱于基于自動(dòng)機(jī)的規(guī)約描述方法，如LTL［5］、CTL［6］等。

2.2基于模型檢驗(yàn)的指揮軟件形式化驗(yàn)證技術(shù)

下一代指揮系統(tǒng)逐漸向網(wǎng)絡(luò)中心化系統(tǒng)發(fā)展，是一個(gè)復(fù)雜人機(jī)系統(tǒng)，常見(jiàn)的系統(tǒng)建模理論和方法包括：Petri網(wǎng)［7］、影響圖［8］、Lanchester方程［9］、多智能體系統(tǒng)［10］以及復(fù)雜網(wǎng)絡(luò)［11］，對(duì)指揮作戰(zhàn)中各要素進(jìn)行建模，生成各種模型，例如：指揮關(guān)系模型、作戰(zhàn)活動(dòng)模型、作戰(zhàn)規(guī)則模型、系統(tǒng)接口模型、系統(tǒng)通信模型等，分析指揮軟件系統(tǒng)中關(guān)鍵性軟件系統(tǒng)的實(shí)時(shí)性、可靠性、可用性、安全性等可信屬性，從作戰(zhàn)視圖、系統(tǒng)視圖、技術(shù)視圖等多個(gè)層次，發(fā)現(xiàn)和提取有待驗(yàn)證的與實(shí)時(shí)性和可用性相關(guān)的可信性質(zhì)。

對(duì)指揮軟件進(jìn)行建模常常涉及到的軟件模型包括：各類UML模型和自動(dòng)機(jī)、Petri網(wǎng)、進(jìn)程代數(shù)等形式化模型。模型檢驗(yàn)技術(shù)包括：面向各類形式模型的檢驗(yàn)技術(shù)、面向各類UML模型的檢驗(yàn)技術(shù)、面向多視圖建模方法的行為一致性檢驗(yàn)技術(shù)、基于前后置謂詞的程序正確性證明技術(shù)。

2.3基于靜態(tài)分析的控制軟件源代碼形式化分析技術(shù)

靜態(tài)分析是指在不運(yùn)行軟件前提下進(jìn)行的分析，對(duì)象一般是針對(duì)程序源代碼，也可以是目標(biāo)代碼?；谠创a的分析一般是基于某個(gè)開(kāi)源編譯器，利用分析前端得到抽象語(yǔ)法樹(shù)，在控制流圖、或數(shù)據(jù)流上進(jìn)行各種類型的分析和檢查。基于格（lattice）和不動(dòng)點(diǎn)（fixpoint）理論的數(shù)據(jù)流分析是目前廣泛采用的技術(shù)：首先對(duì)控制流圖中每個(gè)結(jié)點(diǎn)建立一個(gè)數(shù)據(jù)流等式，并根據(jù)分析目標(biāo)構(gòu)造一個(gè)具有有限高度的格L，然后不斷重復(fù)計(jì)算每個(gè)節(jié)點(diǎn)的輸出，直到達(dá)到格的一個(gè)不動(dòng)點(diǎn)。

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

基于符號(hào)執(zhí)行技術(shù)的程序源代碼分析框架［12］如圖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ù)。

在符號(hào)執(zhí)行框架中，有兩種技術(shù)影響符號(hào)執(zhí)行框架的效率：

1）符號(hào)調(diào)度器。通常基于有向圖搜索策略的不同可以分為：深度遍歷和寬度遍歷。當(dāng)前，符號(hào)調(diào)度器比較有名的研究性成果有EXE、JPF-SE、KLEE等等。

2）約束求解器。是獲取滿足一組約束的解，典型代表性工具有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中。

使用靜態(tài)分析檢測(cè)方法對(duì)控制類軟件程序進(jìn)行檢測(cè)，可以分析內(nèi)存安全性相關(guān)的錯(cuò)誤，例如：內(nèi)存泄漏、空指針解引用、懸掛指針解引用、多次釋放，研究各類Lanchester方程設(shè)計(jì)約束求解器，得到一組能覆蓋各類解算程序所有執(zhí)行路徑的用例，用于軟件測(cè)試過(guò)程，能夠覆蓋所有測(cè)試路徑。

2.4指揮控制軟件形式化分析與驗(yàn)證集成環(huán)境

以上述研究技術(shù)為基礎(chǔ)，設(shè)計(jì)并實(shí)現(xiàn)相應(yīng)的分析與驗(yàn)證集成環(huán)境，用在指揮控制軟件設(shè)計(jì)與開(kāi)發(fā)過(guò)程中，能夠有效對(duì)指揮控制軟件關(guān)鍵模塊進(jìn)行形式化分析與驗(yàn)證，并具有較高的自動(dòng)化程度。指揮控制軟件形式化與驗(yàn)證集成環(huán)境框架如圖2所示，主要包括安全性質(zhì)形式化規(guī)約技術(shù)、基于模型檢驗(yàn)的形式化驗(yàn)證技術(shù)、基于靜態(tài)分析的源代碼形式化分析技術(shù)。底層關(guān)鍵支撐技術(shù)包括性質(zhì)規(guī)約、自動(dòng)模型抽象與驗(yàn)證、C程序語(yǔ)義抽象內(nèi)存模型、基于抽象模型的靜態(tài)檢測(cè)技術(shù)等。

圖2　指揮控制軟件形式化分析與驗(yàn)證集成環(huán)境框架

本項(xiàng)目擬設(shè)計(jì)的驗(yàn)證支撐環(huán)境包括兩部分：①基于模型檢驗(yàn)的驗(yàn)證工具，如圖3所示；②基于內(nèi)存抽象模型的程序靜態(tài)分析工具，如圖4所示。

圖3基于模型檢驗(yàn)的驗(yàn)證框架

圖3給出了本項(xiàng)目擬設(shè)計(jì)的基于模型檢驗(yàn)的程序驗(yàn)證框架。從功能上，該框架主要包括如下2個(gè)模塊：模型抽象算法和模型檢驗(yàn)?zāi)K。

1）模型抽象算法：基于給定的謂詞集合，采用謂詞抽象，從各指揮類軟件設(shè)計(jì)過(guò)程生成的各類模型中抽取有窮狀態(tài)抽象模型（如：布爾程序）；

2）模型檢驗(yàn)?zāi)K：對(duì)抽取出的模型使用模型檢驗(yàn)算法進(jìn)行狀態(tài)搜索，如果性質(zhì)成立，則驗(yàn)證過(guò)程結(jié)束，軟件源代碼滿足給定的性質(zhì)；否則，對(duì)模型檢驗(yàn)算法產(chǎn)生的反例進(jìn)行可行性檢查和處理。

圖4　基于內(nèi)存抽象模型的靜態(tài)程序分析框架

圖4給出了本項(xiàng)目擬設(shè)計(jì)的基于內(nèi)存抽象模型的靜態(tài)程序分析框架［13］。從功能上，該框架包括如下4個(gè)模塊：

1）內(nèi)存抽象模型：針對(duì)堆操作程序關(guān)于指針操作具有局部特性，以與指針指向結(jié)點(diǎn)距離值為分界點(diǎn)精確描述和保守抽象指針的別名關(guān)系，保證分析不產(chǎn)生漏報(bào)，同時(shí)達(dá)到一定的可擴(kuò)展性。

2）內(nèi)存泄露檢測(cè)Memcheck：內(nèi)存泄漏是軟件可信性研究的重要內(nèi)容，同時(shí)是指針操作程序易發(fā)生、難以檢測(cè)的錯(cuò)誤。平凡的指針域操作、各種數(shù)據(jù)結(jié)構(gòu)交織在一起更增加了檢測(cè)它的難度。以內(nèi)存抽象模型為程序狀態(tài)，根據(jù)程序的操作語(yǔ)義對(duì)程序狀態(tài)進(jìn)行遷移，找到各個(gè)程序點(diǎn)關(guān)于程序狀態(tài)的不動(dòng)點(diǎn)，對(duì)控制軟件程序進(jìn)行自動(dòng)檢測(cè)內(nèi)存泄漏錯(cuò)誤。

3）非法指針解引用檢測(cè)Pointercheck：非法指針解引用是軟件可信性研究的另一重要內(nèi)容，它可能會(huì)導(dǎo)致信息泄漏、重要數(shù)據(jù)被篡改或系統(tǒng)崩潰。程序運(yùn)行過(guò)程中表現(xiàn)形式又可以具體分為3種類型：空指針解引用、懸掛指針解引用、多次釋放。這3種類型的錯(cuò)誤既有統(tǒng)一的一面，又有區(qū)別的一面：相同的是指針的值是無(wú)效的（即：所指向的內(nèi)存結(jié)點(diǎn)已經(jīng)被釋放），因此，這3種類型錯(cuò)誤檢測(cè)能夠統(tǒng)一于同一個(gè)抽象模型；不同的是這3種類型發(fā)生的形式不同，這就需要針對(duì)不同語(yǔ)句設(shè)計(jì)違背合法指針解引用規(guī)則進(jìn)行分類檢測(cè)。以內(nèi)存抽象模型為程序遷移狀態(tài)，以3種非法指針解引用發(fā)生的條件為檢測(cè)依據(jù)，對(duì)控制軟件程序進(jìn)行非法指針解引用的算法。

4）數(shù)值性質(zhì)檢測(cè)Numcheck：裝備控制軟件涉及到大量的基于Lanchester方程諸元解算程序，運(yùn)算過(guò)程中這些數(shù)據(jù)在計(jì)算機(jī)中由浮點(diǎn)數(shù)表示的，浮點(diǎn)數(shù)具有非均勻分布特征，并且浮點(diǎn)操作會(huì)引入浮點(diǎn)誤差。盡管單個(gè)浮點(diǎn)操作所帶來(lái)的舍入誤差通常都很小，但如果舍入誤差在長(zhǎng)序列的浮點(diǎn)計(jì)算中不斷累加時(shí)，也可能產(chǎn)生嚴(yán)重后果，甚至導(dǎo)致災(zāi)難性后果。數(shù)值性質(zhì)檢測(cè)將研究如下安全性相關(guān)問(wèn)題：①分析浮點(diǎn)程序是否會(huì)出現(xiàn)上溢、除零錯(cuò)、無(wú)效運(yùn)算等運(yùn)行時(shí)錯(cuò)誤；②分析浮點(diǎn)程序中舍入誤差的傳播情況，并分析程序中舍入誤差的源頭及累計(jì)上界。

3　結(jié)束語(yǔ)

隨著武器裝備信息化程度的提高，軍用軟件的規(guī)模逐漸增大，復(fù)雜度也逐漸增加，在軟件開(kāi)發(fā)各個(gè)階段使用軟件質(zhì)量保證技術(shù)可以增強(qiáng)軟件的可信性，提高武器系統(tǒng)的穩(wěn)定性和可靠性。一方面，應(yīng)該鼓勵(lì)軍用軟件研制單位積極參加第三方軟件開(kāi)發(fā)標(biāo)準(zhǔn)組織的評(píng)定，提高軟件開(kāi)發(fā)能力的提升；另外一方面，使用各種軟件測(cè)試工具盡可能多地對(duì)軟件的功能進(jìn)行正確性測(cè)試，尤其是對(duì)關(guān)鍵和重要模塊設(shè)計(jì)全覆蓋的測(cè)試用例對(duì)其測(cè)試；同時(shí)，鼓勵(lì)軟件開(kāi)發(fā)人員規(guī)范化設(shè)計(jì)文檔，提高軟件理論水平，使用各種軟件分析與驗(yàn)證工具對(duì)軟件的各種模型和代碼進(jìn)行驗(yàn)證和分析，盡可能早地發(fā)現(xiàn)軟件的設(shè)計(jì)缺陷和錯(cuò)誤。

［1］GJB 4072A-2006.軍用軟件質(zhì)量監(jiān)督要求［S］.北京：總裝備部，2006.

［2］Leveson N G.Software Safety:Why，What，and How［J］. Computer Surveys，1986，18（2）：125-163.

［3］GJB 5000A-2008.軍用軟件研制能力成熟度模型［S］.北京：總裝備部，2008.

［4］Paulk M C，Weber，C V，Curtis B et al.Capability Maturity Model for Software,Version 1.1［R］.Technical Report. CMU/SEI-93-TR-024 ESC-TR-93-177，1993.

［5］Pnueli A.The Temporal Logic of Programs［C］//Proc.of 18th IEEE Symposium on Foundation of Computer Science.IEEE Computer Society，1977，46-57.

［6］Emerson E A，Clarke E M.Characterizing Correctness Properties of Parallel Programs Using Fixpoints［C］//Proc.of the 7th Int.Colloquium of Automata,Languages and Programming，1980.

［7］袁崇義.Petri網(wǎng)原理與應(yīng)用［M］.北京：電子工業(yè)出版社，2005.

［8］劉俊先，羅雪山.基于影像圖方法的C4ISR作戰(zhàn)模型［J］.系統(tǒng)工程與電子技術(shù)，2003，25（5）：537-539.

［9］張維明，邱滌洲.C3I系統(tǒng)理論基礎(chǔ)：C3I系統(tǒng)建模方法與技術(shù)［M］.長(zhǎng)沙：國(guó)防科技大學(xué)出版社，2000.

［10］賈子英，楊金照，閆飛龍.防控體系分布式指揮系統(tǒng)研究［J］.現(xiàn)代防御技術(shù)，2013，41（2）：118-122.

［11］朱濤，常國(guó)岑，施笑安.基于復(fù)雜網(wǎng)絡(luò)的指揮信息系統(tǒng)拓?fù)淠Ｐ脱芯浚跩］.系統(tǒng)仿真學(xué)報(bào)，2008，20（6）：1574-1576.

［12］King J C.Symbolic Execution and Program Testing［J］. Journal of the ACM，1976，19（7）：385-394.

［13］董龍明.基于域敏感內(nèi)存抽象模型的堆操作程序靜態(tài)分析［D］.長(zhǎng)沙：國(guó)防科技大學(xué)，2012.

Static Analysis and Verification Technology for Reliability of Military Command and Control Software

XU Jing-Qi1,DONG Long-ming2,HAO Li-bo1
（1.Hunan Mechanical and Electrical Polytechnic,Changsha 410151，China；2.Nanjing Military Representative Office of The General Armament Department，Nanjing 210000，China）

With improving the informatization level of weapon equipment，the reliability of military command and control software is directly related to its overall effectiveness.On basis of the research of traditional software quality assurance technologies，the formal method based software analysis and verification technology are presented according to the characteristic of the military command and control software.It includes：the formal safety specification technology，the verification technology of the command software based on model checking and the analysis technology of the control software based on static analysis.In the end，the formal analysis and verification integrated environment suitable for the life cycle development of the command and control software are put forward.

military command and control software，analysis and verification technology，model checking，static analysis

TP39

A

1002-0640（2015）08-0176-05

2014-07-02

2014-08-07

湖南省科技廳應(yīng)用基礎(chǔ)研究項(xiàng)目（2014FJ3050）；湖南省教育科學(xué)規(guī)劃基金資助項(xiàng)目（XJK013CXX003）

許婧棋（1983-），女，湖南常德人，碩士，講師。研究方向：多目標(biāo)算法與智能控制、軟件工程。