軟件產品線工程通過管理軟件產品的可變性和共性特征,提高軟件開發(fā)效率,節(jié)約開發(fā)成本。模型檢測是一種自動形式化驗證技術。隨著軟件產品線在安全關鍵領域的廣泛應用,對軟件產品線的模型檢測已成為軟件驗證領域的一個重要研究方向。在軟件產品線開發(fā)的早期階段,由于特征的復雜性,系統(tǒng)設計中往往存在不確定信息。然而,現有的軟件產品線模型檢測對這種情況下的建模和驗證支持不足。為此,本文提出一種基于多值邏輯對軟件產品線的不完備設計進行建模和驗證的方法,可以描述軟件產品線設計初期存在的不確定信息,將模型檢測提前到系統(tǒng)開發(fā)的早期階段進行,及時發(fā)現錯誤,降低后期的修復成本。本文的具體工作包括以下幾個方面。首先,本文以世界雙格作為理論基礎,提出一種多值模型——基于雙格的特征遷移系統(tǒng),實現對包含不確定信息的軟件產品線進行建模,并通過投影和精化關系定義特定軟件產品的不完備模型和具體模型。然后,采用動作計算樹邏輯描述系統(tǒng)的時序屬性,定義動作計算樹邏輯在基于雙格的特征遷移系統(tǒng)上的語義,提出基于雙格的多值模型檢測。進一步,為實現基于雙格的多值模型檢測,一方面,提出從基于雙格的特征遷移系統(tǒng)到多值Kripke結構的等價轉換方法,開... 

【文章來源】：南京航空航天大學江蘇省 211工程院校

【文章頁數】：71 頁

【學位級別】：碩士

【文章目錄】：
摘要
ABSTRACT
注釋表
第一章 緒論
    1.1 研究背景
        1.1.1 軟件產品線
        1.1.2 模型檢測
        1.1.3 軟件產品線的模型檢測
    1.2 研究現狀
    1.3 本文研究內容
        1.3.1 軟件產品線的不完備建模
        1.3.2 軟件產品線的多值模型檢測
    1.4 本文組織結構
第二章 預備知識
    2.1 軟件產品線的可變性建模
        2.1.1 特征與特征圖
        2.1.2 遷移系統(tǒng)與特征遷移系統(tǒng)
    2.2 多值模型檢測
        2.2.1 雙格與世界雙格
        2.2.2 多值Kripke結構與CTL邏輯
    2.3 本章小結
第三章 軟件產品線的不完備建模
    3.1 基于雙格的特征遷移系統(tǒng)
    3.2 產品的不完備模型
    3.3 產品的具體模型
    3.4 本章小結
第四章 軟件產品線的多值模型檢測
    4.1 基于BFTS的多值模型檢測
    4.2 多值模型檢測問題的實現
        4.2.1 基于模型轉換的多值模型檢測
        4.2.2 基于模型分解的多值模型檢測
    4.3 本章小結
第五章實驗設計與分析
    5.1 χ Chek簡介
    5.2 BPMCA工具設計
        5.2.1 BPMCA工具的架構設計與實現
        5.2.2 轉換模型與代數格生成算法
        5.2.3 BPMCA工具的使用
    5.3 實例分析
    5.4 本章小結
第六章 總結及展望
    6.1 論文總結
    6.2 未來工作展望
參考文獻
致謝
在學期間的研究成果及發(fā)表的學術論文


【參考文獻】：
期刊論文
[1]軟件產品線可變性建模技術系統(tǒng)綜述[J]. 聶坤明,張莉,樊志強.  軟件學報. 2013(09)
[2]面向軟件產品家族的變化性建模方法[J]. 鄒盛享,張偉,趙海燕,梅宏.  軟件學報. 2005(01)



本文編號：3124190