基于多值邏輯的軟件產品線模型檢測.pdf

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

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