[發(fā)明專利]一種程序不可達(dá)路徑的自動(dòng)檢測(cè)方法

在審

• 申請(qǐng)?zhí)枺?/td>: 201510843266.7
• 申請(qǐng)日: 2015-11-26
• 公開（公告）號(hào): CN105446881A
• 公開（公告）日: 2016-03-30
• 發(fā)明（設(shè)計(jì)）人: 唐鄭熠;王金水;薛醒思;洪茂雄;胡文瑜;劉建華
• 申請(qǐng)（專利權(quán)）人: 福建工程學(xué)院
• 主分類號(hào): G06F11/36
• 分類號(hào): G06F11/36
• 代理公司: 北京市商泰律師事務(wù)所 11255
• 代理人: 王曉彬

1.一種程序不可達(dá)路徑的自動(dòng)檢測(cè)方法，其特征在于，包括如下步驟：

步驟1)將待檢測(cè)的計(jì)算機(jī)程序轉(zhuǎn)化為控制流圖；

步驟2)通過改進(jìn)的廣度優(yōu)先搜索策略將控制流圖轉(zhuǎn)化為程序模型；

步驟3)分析每個(gè)狀態(tài)是否可達(dá)，尋找程序中的不可達(dá)路徑，方法為：驗(yàn)證程序模型中的每個(gè)狀態(tài)s是否存在一條包含s的狀態(tài)序列；若對(duì)于某個(gè)狀態(tài)s，不存在包含s的狀態(tài)序列，則此狀態(tài)為不可達(dá)狀態(tài)；

步驟4)采用模型檢測(cè)技術(shù)自動(dòng)檢測(cè)步驟2)中的程序模型，得到不可達(dá)狀態(tài)的集合；

步驟5)根據(jù)不可達(dá)狀態(tài)的集合，搜索程序路徑是否包含不可達(dá)狀態(tài)，得到不可達(dá)路徑集合。

2.如權(quán)利要求1所述的程序不可達(dá)路徑的自動(dòng)檢測(cè)方法，其特征在于，所述步驟2)中，程序模型為包含狀態(tài)、遷移和遷移標(biāo)號(hào)三大要素的形式化模型，且不包含狀態(tài)、遷移和標(biāo)號(hào)三大要素以外的性質(zhì)要素。

3.如權(quán)利要求1所述的程序不可達(dá)路徑的自動(dòng)檢測(cè)方法，其特征在于，所述改進(jìn)的廣度優(yōu)先搜索策略具體為：

3.1)遍歷控制流圖中的每個(gè)節(jié)點(diǎn)，若該節(jié)點(diǎn)是一個(gè)賦值語句，則創(chuàng)建一個(gè)新的狀態(tài)，并以該賦值語句為遷移標(biāo)號(hào)，創(chuàng)建一個(gè)從前驅(qū)狀態(tài)到新狀態(tài)的遷移；若該節(jié)點(diǎn)是一個(gè)判定語句，則創(chuàng)建兩個(gè)新的狀態(tài)，分別表示判定條件為真和假兩種情況，并依據(jù)判定語句的真假兩種取值情況生成遷移標(biāo)號(hào)；

3.2)若當(dāng)前節(jié)點(diǎn)的后繼節(jié)點(diǎn)是遍歷過的節(jié)點(diǎn)，則創(chuàng)建一個(gè)從當(dāng)前節(jié)點(diǎn)到后繼節(jié)點(diǎn)的前一節(jié)點(diǎn)的空標(biāo)號(hào)遷移；

3.3)記錄每個(gè)節(jié)點(diǎn)所對(duì)應(yīng)的狀態(tài)。

4.如權(quán)利要求1所述的程序不可達(dá)路徑的自動(dòng)檢測(cè)方法，其特征在于，所述步驟5)中，采用遞歸策略搜索程序路徑是否包含不可達(dá)狀態(tài)。

5.如權(quán)利要求4所述的程序不可達(dá)路徑的自動(dòng)檢測(cè)方法，其特征在于，采用遞歸策略搜索程序不可達(dá)路徑的方法具體為：搜索程序模型的所有狀態(tài)，若搜索到的狀態(tài)為終止?fàn)顟B(tài)則遞歸終止，并判斷當(dāng)前生成的路徑中是否包含不可達(dá)狀態(tài)，若包含，則當(dāng)前生成的路徑是不可達(dá)路徑；若搜索到的狀態(tài)不是終止?fàn)顟B(tài)，則將當(dāng)前狀態(tài)加入到程序路徑中，并檢查當(dāng)前狀態(tài)的所有后繼狀態(tài)，若后繼狀態(tài)未出現(xiàn)在程序路徑中，則對(duì)該后繼狀態(tài)繼續(xù)進(jìn)行遞歸。