[發(fā)明專利]一種面向DO?178C軟件測(cè)試過程的目標(biāo)驗(yàn)證及證據(jù)模型提取方法

有效

• 申請(qǐng)?zhí)枺?/td>: 201510419701.3
• 申請(qǐng)日: 2015-07-16
• 公開（公告）號(hào): CN104978275B
• 公開（公告）日: 2017-09-29
• 發(fā)明（設(shè)計(jì)）人: 劉超;楊陽;楊海燕;任健
• 申請(qǐng)（專利權(quán)）人: 北京航空航天大學(xué)
• 主分類號(hào): G06F11/36
• 分類號(hào): G06F11/36
• 代理公司: 北京天達(dá)知識(shí)產(chǎn)權(quán)代理事務(wù)所(普通合伙)11386
• 代理人: 左萌,馬東偉

1.一種面向DO-178C軟件測(cè)試過程的目標(biāo)驗(yàn)證及證據(jù)模型提取方法，具體包括以下步驟：

步驟一、依據(jù)DO-178C標(biāo)準(zhǔn)，建立軟件測(cè)試內(nèi)容的目標(biāo)分解論證模型結(jié)構(gòu)，即GSN模型；

步驟二、依據(jù)GSN模型，分析提取論證GSN模型目標(biāo)的證據(jù)需求，并依據(jù)證據(jù)需求建立類圖形式的證據(jù)模型；

步驟三、將GSN模型依據(jù)論證結(jié)構(gòu)轉(zhuǎn)換為一階謂詞表達(dá)式；

步驟四、依據(jù)GSN模型轉(zhuǎn)換的一階謂詞表達(dá)式對(duì)類圖形式的證據(jù)模型賦值，對(duì)目標(biāo)的滿足性進(jìn)行推理論證，顯示目標(biāo)是否滿足，并分析未能滿足目標(biāo)的原因。

2.根據(jù)權(quán)利要求1所述的面向DO-178C軟件測(cè)試過程的目標(biāo)驗(yàn)證及證據(jù)模型提取方法，其中，所述步驟一進(jìn)一步包括：

GSN模型將最上層的總目標(biāo)進(jìn)行分解，最終分解到可以使用相應(yīng)證據(jù)直接證明的最底層的子目標(biāo)，并連接相應(yīng)證據(jù)，用這一論證結(jié)構(gòu)來說明證據(jù)是如何論證目標(biāo)的。

3.根據(jù)權(quán)利要求1所述的面向DO-178C軟件測(cè)試過程的目標(biāo)驗(yàn)證及證據(jù)模型提取方法，其中，所述步驟二進(jìn)一步包括：

2.1參考GSN表示結(jié)構(gòu)中最底層的子目標(biāo)，確定需要的證據(jù)需求；

2.2參考GSN表示結(jié)構(gòu)中的證據(jù)，以及DO-178C中規(guī)定的輸出以及輸出中包括的數(shù)據(jù)項(xiàng)，將GSN表示結(jié)構(gòu)中的證據(jù)作為類名，將輸出中的數(shù)據(jù)項(xiàng)作為類中的屬性或者方法表示出來；

2.3參考步驟2.1中建立的證據(jù)需求，將步驟2.2中建立的類中的屬性或者方法進(jìn)行修改，添加需要的屬性或者方法，刪除用不到的屬性或者方法；

2.4將依據(jù)證據(jù)自身存在的關(guān)聯(lián)，以及步驟2.1中證據(jù)需求表示的證據(jù)間的關(guān)系，將步驟2.3中各個(gè)證據(jù)類關(guān)聯(lián)起來，建立完整的證據(jù)模型，以類圖的形式表達(dá)出來。

4.根據(jù)權(quán)利要求1所述的面向DO-178C軟件測(cè)試過程的目標(biāo)驗(yàn)證及證據(jù)模型提取方法，其中，所述步驟三進(jìn)一步包括：

3.1將GSN模型中最底層的子目標(biāo)使用規(guī)定的關(guān)鍵句式表達(dá)出來，依據(jù)定義好的轉(zhuǎn)換規(guī)則，將該子目標(biāo)轉(zhuǎn)換成為一階謂詞表達(dá)形式；

3.2將轉(zhuǎn)換成為一階謂詞表達(dá)形式的子目標(biāo)用邏輯關(guān)系連接起來，直到完整表達(dá)出總目標(biāo)為止；

3.3在總結(jié)出完整表達(dá)出總目標(biāo)的一階謂詞表達(dá)式后，將其化簡(jiǎn)得到最終的一階謂詞表達(dá)式。

5.根據(jù)權(quán)利要求1所述的面向DO-178C軟件測(cè)試過程的目標(biāo)驗(yàn)證及證據(jù)模型提取方法，其中，所述步驟四中依據(jù)GSN模型轉(zhuǎn)換的一階謂詞表達(dá)式對(duì)類圖形式的證據(jù)模型賦值進(jìn)一步包括：

將實(shí)際項(xiàng)目數(shù)據(jù)存入證據(jù)模型中作為證據(jù)元素，利用變量對(duì)應(yīng)關(guān)系表，對(duì)一階謂詞邏輯表達(dá)式中的各個(gè)變量與證據(jù)元素中的值進(jìn)行一一對(duì)應(yīng)。

6.根據(jù)權(quán)利要求5所述的面向DO-178C軟件測(cè)試過程的目標(biāo)驗(yàn)證及證據(jù)模型提取方法，其中，所述步驟四中對(duì)目標(biāo)的滿足性進(jìn)行推理論證進(jìn)一步包括：

建立一階謂詞表達(dá)式的自動(dòng)推理機(jī)工具，將一階謂詞表達(dá)式放入自動(dòng)推理機(jī)工具中，產(chǎn)生論證結(jié)果，說明項(xiàng)目數(shù)據(jù)是否符合DO-178C中規(guī)定的目標(biāo)。