軟件產(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)證的方法,可以描述軟件產(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ǔ)義,提出基于雙格的多值模型檢測(cè)。進(jìn)一步,為實(shí)現(xiàn)基于雙格的多值模型檢測(cè),一方面,提出從基于雙格的特征遷移系統(tǒng)到多值Kripke結(jié)構(gòu)的等價(jià)轉(zhuǎn)換方法,開(kāi)... 

【文章來(lái)源】：南京航空航天大學(xué)江蘇省 211工程院校

【文章頁(yè)數(shù)】：71 頁(yè)

【學(xué)位級(jí)別】：碩士

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


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



本文編號(hào)：3124190