軟件形式化是當前構(gòu)建安全可信軟件系統(tǒng)的重要方法之一。由形式化模型驅(qū)動軟件開發(fā)過程中,開發(fā)人員需要首先建立一個形式化的模型并驗證其正確性,然后基于該模型開發(fā)系統(tǒng)的代碼實現(xiàn)。由于技術(shù)所限,目前模型自動轉(zhuǎn)換技術(shù)還不足以幫助技術(shù)人員完全自動化地完成代碼轉(zhuǎn)換工作,轉(zhuǎn)換過程仍然需要涉及大量的人為工作。因此,保證模型與代碼的一致性的任務(wù)必須貫穿整個開發(fā)流程。在理想的情況下,模型是經(jīng)過驗證被認為相對正確的,故只需要使用基于模型的測試方法檢測軟件代碼針對軟件模型的一致性。然而,隨著當今軟件系統(tǒng)規(guī)模的不斷增大,需求變動越來越頻繁,對應(yīng)的軟件開發(fā)流程也變得越來越靈活,代碼有時會先于模型被修改。例如,反向工程或項目重構(gòu)的需要；在需求的臨時變更導致代碼亟需修改；對關(guān)鍵代碼反向抽取模型進行形式化驗證的情況等。傳統(tǒng)的基于模型的測試方法只能檢測代碼之于模型的一致性而不能反作用于模型層面,模型的修改者只能人為地評估修改的正確性,大大降低了模型修改效率并增加了系統(tǒng)的潛在隱患。為此,本文對傳統(tǒng)基于模型的測試方法的一致性檢測進行了擴展,提出了一個可以雙向檢測模型與代碼一致性的框架。該框架通過基于模型的測試從測試結(jié)果中抽取表達... 

【文章來源】：華東師范大學上海市 211工程院校 985工程院校 教育部直屬院校

【文章頁數(shù)】：52 頁

【學位級別】：碩士

【文章目錄】：
摘要
ABSTRACT
第一章 緒論
    1.1 研究背景
    1.2 國內(nèi)外研究現(xiàn)狀
    1.3 關(guān)鍵問題與技術(shù)路線
    1.4 本文的主要貢獻
    1.5 本文的組織結(jié)構(gòu)
第二章 相關(guān)概念介紹
    2.1 形式化建模
    2.2 模型檢測
    2.3 時序邏輯
    2.4 基于模型的測試
    2.5 本章小結(jié)
第三章 一個熱水壺系統(tǒng)實例
    3.1 模型概述
    3.2 系統(tǒng)行為詳述
    3.3 可能出現(xiàn)的不一致情況
    3.4 本章小結(jié)
第四章 雙向一致性檢測
    4.1 基本流程
    4.2 基于模型的測試及其擴展
        4.2.1 測試用例生成
        4.2.2 測試用例擴展
        4.2.3 測試用例執(zhí)行
    4.3 時序邏輯公式抽取
        4.3.1 測試結(jié)果比對與不一致分類
        4.3.2 時序邏輯公式轉(zhuǎn)譯
        4.3.3 時序邏輯公式優(yōu)化
        4.3.4 生成時序邏輯示例
    4.4 與模型檢測工具結(jié)合
    4.5 本章小結(jié)
第五章 雙向一致性檢測框架：ProMiner
    5.1 技術(shù)選型與架構(gòu)
    5.2 組件介紹
    5.3 本章小節(jié)
第六章 實驗分析
    6.1 實驗方法與內(nèi)容
        6.1.1 多功能智能卡系統(tǒng)
        6.1.2 熱水壺系統(tǒng)和電梯系統(tǒng)
    6.2 實驗數(shù)據(jù)
    6.3 結(jié)論與分析
    6.4 本章小結(jié)
第七章 總結(jié)與展望
    7.1 全文總結(jié)
    7.2 后續(xù)工作展望
致謝
參考文獻
附錄 攻讀學位期間發(fā)表的學術(shù)論文


【參考文獻】：
期刊論文
[1]基于Event-B方法的多應(yīng)用智能卡的建模與開發(fā)[J]. 章玥,郭建,朱曉冉,王文君,朱晶洋,湯家華,陳峻念.  計算機工程與科學. 2014(10)
[2]基于模型的開發(fā)方法在多應(yīng)用智能卡中的應(yīng)用[J]. 章玥,郭建,朱曉冉.  信息網(wǎng)絡(luò)安全. 2013(12)
[3]元建模技術(shù)研究進展[J]. 劉輝,麻志毅,邵維忠.  軟件學報. 2008(06)
[4]面向模型檢驗的UML狀態(tài)機語義[J]. 周穎,鄭國梁,李宣東.  電子學報. 2003(S1)
[5]基于UML狀態(tài)圖的類測試用例自動生成方法[J]. 張毅坤,施鳳鳴,姚全珠,劉軍,付長龍.  計算機工程. 2003(21)
[6]模型檢測:理論、方法與應(yīng)用[J]. 林惠民,張文輝.  電子學報. 2002(S1)

碩士論文
[1]模型和代碼的一致性檢測方法的研究[D]. 王翠欽.重慶大學 2014



本文編號：3446984