航天器軟件典型缺陷模式的自動檢測技術(shù)

高 猛，滕俊元，陳 睿，孫 民

0 引 言

我國新一代航天器中廣泛采用軟件密集系統(tǒng)(software-intensive system)，軟件在保證航天器安全穩(wěn)定運行、可靠完成任務(wù)方面起著至關(guān)重要的作用.航天器許多關(guān)鍵任務(wù)的完成均依賴于軟件，軟件規(guī)模和復(fù)雜度呈幾何級增長，這種特點和趨勢在空間站、載人航天、深空探測等重大航天工程中尤為凸顯.

同時，航天器屬于典型的安全苛求系統(tǒng)，軟件一旦發(fā)生失效，將會導(dǎo)致任務(wù)失敗或人員傷亡.例如，某飛控軟件由于未及時清除噴氣標志導(dǎo)致發(fā)動機持續(xù)噴氣，險些導(dǎo)致火箭發(fā)射失利.經(jīng)統(tǒng)計，近十年五院航天器在軌首次異常中軟件因素約占15%、在研質(zhì)量問題中軟件因素約占20%，航天器軟件質(zhì)量問題頻發(fā)且呈上升趨勢.軟件安全性已成為航天型號任務(wù)中最為關(guān)鍵的風(fēng)險因素之一.

另外，隨著航天器軟件缺陷數(shù)據(jù)的逐步積累，如何利用這些缺陷數(shù)據(jù)提高軟件可靠性安全性是軟件從業(yè)人員必須思考的問題.典型多發(fā)問題的規(guī)避和檢測是實現(xiàn)軟件質(zhì)量提升的重要途徑.統(tǒng)計表明，絕大多數(shù)航天器軟件問題都是已知類型的缺陷模式[1-2]，符合“二八原則”規(guī)律，即約80%的問題分布于20%的缺陷類型中，如時序沖突問題、數(shù)據(jù)競爭問題、可靠性設(shè)計問題、數(shù)據(jù)取值范圍相關(guān)問題(如數(shù)組越界、除零、數(shù)據(jù)溢出、變量未初始化等)等.

本文通過系統(tǒng)分析和總結(jié)航天器軟件典型多發(fā)問題，開展軟件缺陷模式研究，建立航天器軟件缺陷模式集；研究缺陷模式的形式化規(guī)約和自動檢測技術(shù)，開發(fā)缺陷模式自動檢測工具，提高缺陷檢出率，從而有效規(guī)避型號中的典型多發(fā)問題，提高航天器軟件研制質(zhì)量、縮短研制周期.

1 軟件缺陷模式研究

軟件缺陷是生存周期內(nèi)所有存在于軟件(文檔、數(shù)據(jù)、程序)之中不正確的，或者是不可接受的需求、設(shè)計、編碼和數(shù)據(jù)結(jié)構(gòu)等.而軟件缺陷模式[3]是指對特定類型的重復(fù)或者類似的軟件缺陷的抽象描述，是從實踐經(jīng)驗中精煉、抽象而出的缺陷類型.目前傳統(tǒng)的軟件缺陷分類體系[4](如IEEE軟件異常分類、Thayer分類標準、缺陷正交分類ODC標準等)不針對某類具體軟件開發(fā)語言進行劃分，具有良好的通用性，但由于其缺陷抽象程度較高，且缺乏具體實例的支持，具有一定的使用難度.因此，需要結(jié)合上述分類方法的優(yōu)點并結(jié)合航天器軟件特點，對航天器軟件缺陷模式分類，為軟件缺陷的檢測、定位、修復(fù)以及預(yù)防提供準確完整的信息.

1.1 缺陷模式獲取

航天器軟件缺陷數(shù)據(jù)來源及獲取主要有2個方面：

a) 型號在軌/在研軟件質(zhì)量問題和研制過程中出現(xiàn)的典型問題；

b) 型號軟件第三方測試問題.

針對上述缺陷數(shù)據(jù)處理過程如圖1所示，首先對缺陷數(shù)據(jù)進行清洗，將不完整的缺陷描述或錯誤的缺陷描述盡量給予修復(fù)，修復(fù)不了的從數(shù)據(jù)源中剔除；其次根據(jù)缺陷產(chǎn)生原因及特性對軟件缺陷進行按類劃分構(gòu)成缺陷數(shù)據(jù)庫；之后，采用統(tǒng)計的方法，對缺陷數(shù)據(jù)庫進行統(tǒng)計合并，相同類型的缺陷合并；最后，從重復(fù)的、類似的缺陷數(shù)據(jù)中抽象出缺陷模式.

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

1.2 缺陷模式描述

為了更好地定義軟件缺陷模式，便于軟件人員理解和應(yīng)用，對軟件缺陷模式進行規(guī)范化描述.本文從航天器軟件工程實踐出發(fā)約定軟件缺陷模式描述規(guī)范，通過定義如下10元組模型來描述航天器軟件缺陷模式屬性，具體如表1所示.

表1 航天器軟件缺陷模式描述規(guī)范Tab.1 Defect pattern specification of spacecraft software

1.3 航天器軟件缺陷模式集

根據(jù)航天器軟件結(jié)構(gòu)化設(shè)計模式和所實現(xiàn)的功能需求與非功能性需求(如可靠性和安全性、實時性處理等要求)，對航天器軟件缺陷模式進行分類.基于面向?qū)ο蟮乃枷?，抽象?1類航天器軟件缺陷模式，如表2所示.

表2 航天器軟件缺陷模式類別Tab.2 Defect pattern category of spacecraft software

同時，為了更好地組織軟件缺陷模式，從不同粒度表達軟件缺陷，本文采用層次化模型描述航天器軟件缺陷模式.將軟件缺陷模式劃分為3層，內(nèi)容如下：

a) 缺陷模式類別：缺陷模式類別是若干同類缺陷模式的統(tǒng)稱，如初始化/復(fù)位類、計算/算法類、中斷/時序設(shè)計類等；

b) 基礎(chǔ)缺陷模式：刻畫一種相對具體的缺陷形式，如變量聲明錯誤等；

c) 缺陷子模式：是基礎(chǔ)缺陷模式的細分，如變量作用域聲明錯誤、局部變量類型聲明錯誤、指針變量類型聲明錯誤均源于變量聲明錯誤的基礎(chǔ)缺陷模式.

本文共梳理總結(jié)軟件基礎(chǔ)缺陷模式123項、缺陷子模式170項，形成并建立首個航天器軟件缺陷模式集，命名為Spacecraft Software Defect Patterns Set(SSDPS).航天器軟件缺陷模式集將實現(xiàn)動態(tài)維護，將通過吸收典型案例及常見多發(fā)問題實現(xiàn)持續(xù)完善.航天器軟件缺陷模式集(部分示例)如表3所示.

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

2 缺陷模式自動檢測技術(shù)研究

2.1 缺陷模式形式化建模

自然語言描述的軟件缺陷模式無法在計算機中表達、存儲、組織以及自動化使用.為了解決該問題，本文采用模型檢測技術(shù)中用于描述程序性質(zhì)的模態(tài)/時序邏輯描述語言對軟件缺陷模式進行形式化描述，以獲取程序性質(zhì)規(guī)約.

航天器軟件系統(tǒng)作為典型的并發(fā)系統(tǒng)，其運行過程和行為可以抽象為狀態(tài)轉(zhuǎn)移系統(tǒng)，程序性質(zhì)則可以通過計算樹邏輯(CTL -Computation Tree Logic)進行刻畫.計算樹邏輯是一種典型的模態(tài)/時序邏輯描述語言，可以描述狀態(tài)的前后關(guān)系和分支情況，屬于分叉時序邏輯.對于CTL，使用路徑量詞(包括：A、E)和模態(tài)算子(包括：F、G、X、U)對程序性質(zhì)進行形式化描述[5].其中，量詞A(Always)和E(Exists)描述分支情況，分別表示全部計算路徑存在和某條計算路徑存在；模態(tài)算子描述狀態(tài)的前后關(guān)系，如表4所示.

本文以表3中“SSDPS-CALC-005：無符號型整數(shù)減操作溢出”為例介紹軟件缺陷模式形式化描述過程.

1) 機理分析：根據(jù)SSDPS-CALC-005缺陷描述可獲知該缺陷產(chǎn)生機理，即：當對一個無符號整數(shù)進行算術(shù)減操作時，使得其結(jié)果取值超過了相應(yīng)類型的最大值[6].因此，若x、y均為無符號整數(shù)，則表達式“x-y”發(fā)生無符號型整數(shù)減操作溢出缺陷的性質(zhì)約束條件為“x

2) 形式化語言描述：如果需要判定是否存在無符號型整數(shù)減操作溢出，需要對整個程序進行遍歷，若某條計算路徑中存在表達式滿足性質(zhì)約束條件“x

通過上述方式，可以基于CTL語言對基礎(chǔ)缺陷模式“無符號型整數(shù)溢出超限”進行如表5所示的形式化描述.

2.2 缺陷模式自動檢測技術(shù)

軟件缺陷模式檢測涉及的程序分析技術(shù)[7-8]主要包括：直接檢索符號表、遍歷抽象語法樹(AST-Abstract Syntax Tree)進行模式匹配、類型檢查、數(shù)據(jù)流分析、抽象解釋、符號執(zhí)行等.限于篇幅，本文重點對符號執(zhí)行技術(shù)進行說明.

符號執(zhí)行技術(shù)[9]是將系統(tǒng)的原始邏輯轉(zhuǎn)換成符號邏輯，根據(jù)符號邏輯來模擬程序執(zhí)行并得到所有執(zhí)行狀態(tài)，分析結(jié)果精確，主要用于查找邏輯復(fù)雜和發(fā)生條件苛刻的軟件缺陷.

在符號執(zhí)行過程中，每當遇到判斷與跳轉(zhuǎn)語句時，符號執(zhí)行分析引擎便會將當前執(zhí)行路徑的路徑約束收集到該路徑的約束集合中.其中，路徑約束(Path Constraint)是指程序分支指令中與輸入符號相關(guān)的分支條件的取值，是一系列不具有量詞的布爾型公式.而路徑約束集合則被用來存儲每一條程序路徑上收集到的約束，用“與”操作進行連接，通過使用約束求解器(Constraint Solver)對約束集合進行求解，可以得到該條路徑的可達性：如果約束求解的結(jié)果有解，表示該條路徑可達，否則表示該條路徑不可達.在時間與計算資源足夠的理想情況下，符號執(zhí)行能夠遍歷目標程序的所有路徑并判斷其可達性.

本文通過在程序特定狀態(tài)點處增加性質(zhì)約束條件，聯(lián)合路徑約束求解實現(xiàn)軟件缺陷模式檢測，具體流程如圖2所示.

圖2 基于符號執(zhí)行的缺陷模式自動檢測流程Fig.2 Automatic defect pattern detection process based on symbolic execution

首先，將被分析C程序?qū)ο蟾鶕?jù)抽象語法樹(AST)構(gòu)造控制流圖(CFG-Control Flow Graph)，控制流圖是編譯器內(nèi)部用有向圖表示一個程序過程的一種抽象數(shù)據(jù)結(jié)構(gòu)，圖中的節(jié)點表示一個程序基本塊，基本塊是沒有任何跳轉(zhuǎn)的順序語句代碼塊，圖中的邊表示代碼中的跳轉(zhuǎn)，它是有向邊.在CFG的基礎(chǔ)上生成符號執(zhí)行樹，并為每一條路徑建立一系列以輸入數(shù)據(jù)為變量的符號表達式.

之后，根據(jù)軟件缺陷模式需要判定的程序性質(zhì)添加相應(yīng)的安全規(guī)則和約束.例如，如果要添加緩沖區(qū)溢出的安全約束，則在執(zhí)行時遇到對內(nèi)存進行操作的語句時，就要對該語句所操作的內(nèi)存對象的邊界添加安全約束.通過上述方式完成軟件安全約束的添加.

最后，分析引擎按照控制流程圖訪問每條語句，并獲得程序中每條語句的符號變量及約束信息，并在每次添加安全約束之后使用約束求解器對所有的安全約束進行求解，以判定當前是否可能潛在一個安全問題，即依據(jù)求解結(jié)果判定是否滿足某個缺陷模式對應(yīng)的程序性質(zhì).

本文以無符號型整數(shù)減操作導(dǎo)致溢出為例，示例程序及基本檢測流程如圖3所示.從檢測流程可以看出，符號執(zhí)行會在模擬執(zhí)行過程中的特定狀態(tài)點，通過對目標符號進行求解，并與缺陷預(yù)期進行比較來暴露出問題.

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

對程序中使用的變量進行符號表示后，針對無符號型整數(shù)減溢出方面的錯誤可以通過將該缺陷模式的性質(zhì)約束條件進行求解，如表6所示.

表6 無符號型整數(shù)減溢出實例Tab.6 Unsigned integer overflow Instance

檢測流程：

1) 檢測所有的“-”、“-=”二元運算符.

2) 獲取二元運算符的左操作數(shù)lhs，右操作數(shù)rhs.

3) 如果lhs或rhs都不是污點數(shù)據(jù)，則獲取lhs和rhs的符號值，根據(jù)二元操作符，將被減數(shù)與減數(shù)進行比較，看約束求解的結(jié)果就可以檢測出無符號型整數(shù)是否溢出.在圖2的示例中根據(jù)我們總結(jié)出的程序性質(zhì)約束條件(S1

2.3 工具設(shè)計與實現(xiàn)

本文基于軟件缺陷模式自動檢測技術(shù)的研究，完善了靜態(tài)分析工具SpecChecker的功能，用于實現(xiàn)典型缺陷模式的自動化檢測.圖4描述了SpecChecker的體系結(jié)構(gòu)，其主要由預(yù)處理、擴展層、配置&調(diào)度層、數(shù)據(jù)層、用戶界面組成.在整個框架中，預(yù)處理層為公共基礎(chǔ)層，為上層所有引擎正常調(diào)度執(zhí)行提供支撐；擴展層主要是為支持更多的缺陷模式類型和分析引擎集成提供接口；配置和調(diào)度層主要根據(jù)語言、編譯平臺、編碼標準等對引擎進行調(diào)度，并通過自定義適配器，將分析結(jié)果適配到統(tǒng)一結(jié)果模型中；數(shù)據(jù)層包括了各個分析引擎產(chǎn)生的所有中間數(shù)據(jù)結(jié)果及最終分析結(jié)果，結(jié)合缺陷類型，為GUI層的結(jié)果展示提供數(shù)據(jù).

圖4 缺陷模式自動檢測工具架構(gòu)Fig.4 The architecture of automated defect pattern detection tools

缺陷模式檢測和分析過程主要分兩個階段.

第一階段，確定被分析源文件及編譯器配置，對每個C文件進行預(yù)處理，生成預(yù)處理后的中間文件；預(yù)處理成功后再對每個中間文件進行語法分析，基于中間表示構(gòu)造器，產(chǎn)生“中間表示”并緩存于分析上下文中，這些“中間表示”主要包括抽象語法樹AST、全局符號表、控制流程圖CFG、函數(shù)調(diào)用圖等.

第二階段，“中間表示”生成后，將根據(jù)已定義的編碼規(guī)則或缺陷模式，調(diào)用相應(yīng)的檢查器對每個C文件對應(yīng)的中間表示進行一系列的分析操作，如果發(fā)現(xiàn)編碼規(guī)則違反或典型缺陷模式，將會把缺陷涉及的詳細信息(被分析文件、缺陷發(fā)生的行號、列號、違反或缺陷提示信息)提交給分析上下文中的錯誤管理模塊.根據(jù)編碼規(guī)則或缺陷模式的定義類型、作用域范圍的不同，檢查機理和算法也有所差異.

目前，工具已支持116項航天器軟件典型缺陷模式的自動檢測.其中，部分示例如表7所示.

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

3 實驗結(jié)果

為驗證基于軟件缺陷模式的自動檢測工具在實際項目中的使用效果，選取某型號四個典型航天嵌入式軟件為對象進行實驗應(yīng)用，檢測范圍為表5中提出的116項航天器軟件典型缺陷模式.

1) 上升器PIU軟件：處理器為80C32，編譯配置為Keil C51，編程語言為C語言，規(guī)模(LOC)為4485行，主要完成工程參數(shù)的采集、遙控指令的執(zhí)行、蓄電池安時計電量累計、蓄電池組充電切換功能、蓄電池組過壓、過放保護等功能.

2) 微波雷達DSP軟件：處理器為SMJ320C6701，編譯配置為TI Code Composer Studio2.2，編程語言為C語言，規(guī)模(LOC)為3493行，主要完成地檢注入數(shù)據(jù)，完成測距、測速數(shù)據(jù)處理、校時功能、程序自檢功能以及DSP自動監(jiān)測重配置功能.

3) 中心控制單元應(yīng)用軟件：處理器為TSC695F，編譯配置為ERC32(SPARC V7)，編程語言為C語言，規(guī)模(LOC)為29401行，實現(xiàn)軌道器各階段的姿態(tài)與軌道控制以及導(dǎo)航和制導(dǎo)任務(wù).

4) CRDS敏感器應(yīng)用軟件：處理器為SOC2008，編譯配置為GNU工具包RCC，編程語言為C語言，規(guī)模(LOC)為8672行，主要完成目標相對位置和相對姿態(tài)角等信息測量.

表8給出了每個被分析軟件的實驗結(jié)果.

表8 被分析項的實驗結(jié)果Tab.8 The experimental results of the analyzed software

從實驗結(jié)果中可以看出：

1) 缺陷模式自動檢測工具的缺陷檢出率超過90%；

2) 工具能夠適應(yīng)于各種編譯配置下的軟件缺陷模式自動檢測；

3) 對于規(guī)模較大的軟件，如GNC子系統(tǒng)中心控制單元應(yīng)用軟件，工具也能很好的支持.

4 結(jié)論與展望

如何更好地了解、掌握航天器軟件缺陷產(chǎn)生和發(fā)展的規(guī)律，控制和減少軟件缺陷造成的影響是航天嵌入式軟件工程領(lǐng)域致力解決的重要問題.鑒于此，本文通過系統(tǒng)分析和總結(jié)航天器軟件典型多發(fā)問題，建立首個航天器軟件缺陷模式集SSDPS；通過時序邏輯語言CTL對軟件缺陷模式進行形式化描述，同時開展了以符號執(zhí)行為代表的缺陷模式自動檢測技術(shù)研究，完成了缺陷模式自動檢測工具SpecChecker的設(shè)計與實現(xiàn).實驗結(jié)果表明，SpecChecker能夠支持大規(guī)模軟件的問題檢測，缺陷檢出率超過90%.目前該工具已在空間站、載人航天、深空探測、北斗導(dǎo)航等國家重大航天型號任務(wù)的第三方評測中進行了全面應(yīng)用.

后續(xù)課題組將持續(xù)完善航天器軟件缺陷模式并不斷將其固化到缺陷模式自動檢測工具中.另一方面，根據(jù)航天器軟件缺陷模式，進一步研究基于專家系統(tǒng)的軟件缺陷預(yù)測模型構(gòu)建技術(shù)和基于機器學(xué)習(xí)的軟件缺陷預(yù)測模型構(gòu)建技術(shù)，利用人工智能開展軟件缺陷的預(yù)測和定位.