基于多值邏輯的軟件產(chǎn)品線模型檢測(cè).pdf

1、軟件產(chǎn)品線工程通過(guò)管理軟件產(chǎn)品的可變性和共性特征，提高軟件開(kāi)發(fā)效率，節(jié)約開(kāi)發(fā)成本。模型檢測(cè)是一種自動(dòng)形式化驗(yàn)證技術(shù)。隨著軟件產(chǎn)品線在安全關(guān)鍵領(lǐng)域的廣泛應(yīng)用，對(duì)軟件產(chǎn)品線的模型檢測(cè)已成為軟件驗(yàn)證領(lǐng)域的一個(gè)重要研究方向。在軟件產(chǎn)品線開(kāi)發(fā)的早期階段,由于特征的復(fù)雜性,系統(tǒng)設(shè)計(jì)中往往存在不確定信息。然而,現(xiàn)有的軟件產(chǎn)品線模型檢測(cè)對(duì)這種情況下的建模和驗(yàn)證支持不足。為此，本文提出一種基于多值邏輯對(duì)軟件產(chǎn)品線的不完備設(shè)計(jì)進(jìn)行建模和驗(yàn)證的方法，可以描述

2、軟件產(chǎn)品線設(shè)計(jì)初期存在的不確定信息，將模型檢測(cè)提前到系統(tǒng)開(kāi)發(fā)的早期階段進(jìn)行，及時(shí)發(fā)現(xiàn)錯(cuò)誤，降低后期的修復(fù)成本。
　　本文的具體工作包括以下幾個(gè)方面。首先，本文以世界雙格作為理論基礎(chǔ)，提出一種多值模型——基于雙格的特征遷移系統(tǒng)，實(shí)現(xiàn)對(duì)包含不確定信息的軟件產(chǎn)品線進(jìn)行建模，并通過(guò)投影和精化關(guān)系定義特定軟件產(chǎn)品的不完備模型和具體模型。然后，采用動(dòng)作計(jì)算樹(shù)邏輯描述系統(tǒng)的時(shí)序?qū)傩?，定義動(dòng)作計(jì)算樹(shù)邏輯在基于雙格的特征遷移系統(tǒng)上的語(yǔ)義，提出基于雙