[發(fā)明專利]一種航天嵌入式C語言軟件運行時錯誤的靜態(tài)分析方法

有效

• 申請?zhí)枺?/td>: 201110291315.2
• 申請日: 2011-09-29
• 公開（公告）號: CN102508766A
• 公開（公告）日: 2012-06-20
• 發(fā)明（設計）人: 王崑聲;詹海潭;經(jīng)小川;張剛;李寧
• 申請（專利權(quán)）人: 中國航天科技集團公司第七一〇研究所
• 主分類號: G06F11/36
• 分類號: G06F11/36
• 代理公司: 中國航天科技專利中心 11009
• 代理人: 臧春喜

技術(shù)領(lǐng)域

本發(fā)明涉及一種航天嵌入式C語言軟件運行時錯誤的靜態(tài)分析方法，屬于軟件測試技術(shù)領(lǐng)域。

背景技術(shù)

目前在航天領(lǐng)域，C語言被普遍應用于編寫嵌入式軟件，C語言已經(jīng)成為嵌入式系統(tǒng)高級編程語言的標準。C語言有很多優(yōu)點但是對于開發(fā)高安全軟件來說它缺少必要的安全措施，主要缺陷有：C語言的非強制類型特性降低了它的可靠性；C語言的另一個特性是沒有對指針操作進行嚴格的限定；此外，C語言不提供對數(shù)組和字符串的邊界檢查。正是由于C語言的這些缺陷，C程序中會存在一些漏洞和錯誤，其中一類為運行時錯誤。運行時錯誤(Run-time?Error)就是軟件在動態(tài)運行時出現(xiàn)的錯誤。根據(jù)ANSIC定義，運行時錯誤是指那些能導致預定義之外的不正確結(jié)果或者處理器停機的錯誤。

運行時錯誤是所有軟件錯誤中最具風險的，同時也是最難發(fā)現(xiàn)的。對于航空航天、汽車以及醫(yī)療設備等安全級別要求非常高的系統(tǒng)來說，一旦出現(xiàn)這樣的運行時錯誤，損失就是不可估量的。

對運行時錯誤進行檢測的方法主要有動態(tài)測試和靜態(tài)分析兩種。動態(tài)測試是傳統(tǒng)的方法，通過軟件的實際執(zhí)行來發(fā)現(xiàn)軟件中的錯誤。其檢測結(jié)果高度依賴于測試用例的選擇，同時，由于只能對有限的測試用例進行檢查，所以動態(tài)測試方法不能保證發(fā)現(xiàn)軟件的所有安全漏洞。靜態(tài)分析方法是在程序不執(zhí)行的狀態(tài)下，通過對被檢測軟件進行建模，發(fā)現(xiàn)滿足所有可能執(zhí)行狀態(tài)的軟件屬性，再通過對事先預定的規(guī)則庫的分析來檢測軟件中的錯誤漏洞。

靜態(tài)分析主要有定理證明，模型驗證和抽象解釋等方法。定理證明和模型檢驗都屬于形式化驗證方法，可以精確地確定軟件的屬性。定理證明方法將程序轉(zhuǎn)換為邏輯公式，然后使用公理和規(guī)則證明程序是一個合法的定理。由于定理證明過程難以完全自動化，需要高素質(zhì)分析人員的大量參與，證明過程非常耗時費力，一般只用于驗證設計階段的程序規(guī)范而非實際代碼。模型檢驗用狀態(tài)遷移系統(tǒng)(S)描述軟件的行為，用時序邏輯、計算樹邏輯或μ-演算公式(F)表示軟件執(zhí)行必須滿足的性質(zhì)，通過自動搜索S中不滿足公式F的狀態(tài)來發(fā)現(xiàn)軟件中的漏洞。由于需要窮盡程序的所有實際執(zhí)行狀態(tài)，所以模型檢驗的效率很低，并且不能檢驗無窮狀態(tài)系統(tǒng)。抽象解釋是用于構(gòu)造和逼近程序不動點語義的理論，它使用抽象對象域上的計算抽象來逼近程序指稱的具體對象域上的計算，使得程序抽象執(zhí)行的結(jié)果能夠反映出程序真實運行的部分信息。它僅跟蹤用戶關(guān)心的程序?qū)傩裕运鼘Τ绦蛘Z義的解釋是程序?qū)嶋H語義的近似。錯誤檢測的兩個標準是準確度和效率。靜態(tài)分析各個方法都有自己的局限性，定理證明和模型驗證方法的準確度比較高，但效率卻比較低。抽象解釋方法的效率比較高，但準確度卻比較低。如何在準確度和效率上取得一個好的平衡是靜態(tài)分析的難點，也是目前研究熱點。

發(fā)明內(nèi)容

本發(fā)明的技術(shù)解決問題是：克服現(xiàn)有技術(shù)的不足，提供了一種航天嵌入式C語言軟件運行時錯誤的靜態(tài)分析方法。采用本發(fā)明提高了對航天嵌入式C語言軟件運行時錯誤進行檢測的準確度和效率。

本發(fā)明的技術(shù)解決方案是：

本發(fā)明所述的一種航天嵌入式C語言軟件運行時錯誤的靜態(tài)分析方法，通過以下步驟實現(xiàn)：

(1)對航天嵌入式C語言軟件運行時錯誤進行分類，按照分類后每類錯誤的屬性模式構(gòu)造屬性狀態(tài)機，所述屬性狀態(tài)機包括程序運行過程中可能出現(xiàn)的屬性狀態(tài)D_i，i＝{1，…n}，n為每類錯誤中的屬性狀態(tài)總數(shù)，D_i包括程序運行過程中可能的出現(xiàn)的錯誤狀態(tài)；

(2)按照程序的控制流程圖和運行時錯誤的屬性狀態(tài)機，根據(jù)控制流程圖中位置l處的節(jié)點信息和輸入屬性狀態(tài)σ_{l_in}，獲得經(jīng)位置l處的節(jié)點處理后的輸出屬性狀態(tài)σ_{l_out}和路徑條件C_s，l，其中，s為到達位置l處的路徑；

(3)判斷σ_{l_out}與屬性狀態(tài)D_i的關(guān)系：

若σ_{l_out}為D_i中的錯誤狀態(tài)，則將路徑條件C_s，l作為可能出現(xiàn)的錯誤提示輸出，并不再對C_s，l進行后續(xù)分析；否則，將σ_{l_out}作為下一個位置處的輸入屬性狀態(tài)返回步驟(2)，直到程序出口。