[發明專利]一種基于模型檢驗的時序軟件質量缺陷檢測方法及系統

有效

• 申請號: 201010150917.1
• 申請日: 2010-04-19
• 公開（公告）號: CN101833504A
• 公開（公告）日: 2010-09-15
• 發明（設計）人: 張翀斌
• 申請（專利權）人: 張翀斌
• 主分類號: G06F11/36
• 分類號: G06F11/36
• 代理公司: 北京安博達知識產權代理有限公司 11271
• 代理人: 徐國文

1.一種基于模型檢驗的時序軟件質量缺陷檢測方法，其特征在于：所述方法的具體步驟如下：

步驟A、輸入被檢測源代碼，并根據所述被檢測源代碼選擇缺陷模式；

步驟B、對所述被檢測的源代碼進行預處理；

步驟C、對合并完的源代碼模型進行控制流圖壓縮；

步驟D、判斷所說缺陷模式的自動機中的終止狀態在所述被檢測的原程序的建模中相對應的安全模型中是否可達，如果所述終止狀態可達，判斷所述被檢測的源代碼程序存在缺陷；如果所述終止狀態不可達，則判斷所述被檢測的源代碼程序不存在缺陷；

步驟E、結果處理：將步驟D中檢測完的源程序代碼終止狀態的位置信息轉換為于原始源代碼的位置信息；

步驟F、輸出：將最終的判斷結果輸出顯示出來供用戶閱讀。

2.根據權利要求1所述的一種基于模型檢驗的時序軟件質量缺陷檢測方法，

其特征在于：所述步驟B包括：

B1、分析所述被檢測的源代碼文件，并生成控制流圖；

B2、如果所述被檢測的源代碼程序由多個代碼文件組成，則先生成各自的控制流圖，再將控制流圖文件合并成一個全局控制流圖文件；

B3、根據生成的控制流程圖建模。

3.根據權利要求1所述的一種基于模型檢驗的時序軟件質量缺陷檢測方法，其特征在于：所述步驟C中壓縮包括：

C1、將所述被檢測的源代碼模型里與所述缺陷模式沒有關系的內容刪除；

C2、將狀態等價的所述源代碼模型合并。

4.根據權利要求1所述的一種基于模型檢驗的時序軟件質量缺陷檢測方法，其特征在于：所述步驟C中所述被檢測源代碼根據在所述步驟A中所選擇的缺陷模式進行源代碼模型壓縮。

5.一種基于模型檢驗的時序軟件質量缺陷檢測系統，其特征在于：所述系統包括源代碼模型生成器、時序缺陷模式庫、源代碼模型壓縮器、時序模型檢驗器和結果生成模塊，所述時序缺陷模式庫連接源代碼模型生成器和時序模型檢驗器，所述源代碼模型生成器經所述源代碼模型壓縮器連接時序模型檢驗器，所述時序模型檢驗器通向結果生成模塊。

6.根據權利要求5所述的一種基于模型檢驗的時序軟件質量缺陷檢測系統，其特征在于：所述源代碼模型生成器將被檢測源代碼的轉化為一種形式化的狀態自動機模型。

7.根據權利要求5所述的一種基于模型檢驗的時序軟件質量缺陷檢測系統，其特征在于：所述時序缺陷模式庫用于存儲時序缺陷并用形式化語言對所述時序缺陷描述建模，從而形成用于檢測的時序缺陷模式。

8.根據權利要求7所述的一種基于模型檢驗的時序軟件質量缺陷檢測系統，其特征在于：所述源代碼模型壓縮器使用時序缺陷模式對被檢測的程序系統模型進行壓縮。

9.根據權利要求5所述的一種基于模型檢驗的時序軟件質量缺陷檢測系統，其特征在于：所述時序模型檢驗器將壓縮后的源代碼模型與所述缺陷模式進行對比檢驗，判斷所述被檢測程序是否違背了缺陷模式。

10.根據權利要求5所述的一種基于模型檢驗的時序軟件質量缺陷檢測系統，其特征在于：所述結果生成模塊將時序模型檢驗器的輸出轉化為檢測人員能易懂的形式。