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

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

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