本文關鍵詞：模型精化過程中模型間一致性檢測研究

  更多相關文章： 模型精化 模型檢測 一致性檢測 屬性抽取 線性時序邏輯

【摘要】：模型精化是軟件工程中基于模型驅動開發(fā)的關鍵問題之一,被廣泛應用于基于模型驅動開發(fā)方法中。若在初始模型中引入過多細節(jié)會使得開發(fā)和測試不易管理,因此對于那些大型復雜系統(tǒng)的建模很難做到一步到位,在實際的開發(fā)建模過程中往往采用模型精化的技術。所謂模型精化即在原模型的基礎上添加更多的細節(jié),逐步細化,模型從剛開始的比較抽象變得逐漸具體化。如何保證模型精化過程中模型間的一致性,一直是工業(yè)界和學術界高度關注的問題之一。模型精化過程中模型間的一致性是正確建模的必要前提,為了保證精化后的模型和精化前是一致的,需要對精化前后的模型進行一致性檢驗。由于模型具有復雜性和抽象性,包含不一致信息的模型將導致開發(fā)后期階段編碼的矛盾和錯誤,一致性檢驗的重要意義就在于可以在軟件設計的早期階段發(fā)現(xiàn)不一致問題,減少生成代碼后出錯所產(chǎn)生的代價。傳統(tǒng)的模型精化過程中模型間一致性檢測方法只關注于模型自身的語法、語義、結構方面的正確性,死鎖(Deadlock)檢測,不變式(Invariants)保持性檢測等,而不關注于模型間行為方面的一致性檢測。然而,系統(tǒng)模型間的不一致往往存在于系統(tǒng)行為的各個方面,使用傳統(tǒng)的一致性檢測方法很難一一找出這些不一致。為此,本文提出利用系統(tǒng)行為屬性來刻畫系統(tǒng)行為狀態(tài)的改變,并結合模型檢測的方法來檢測模型間的行為一致性。我們假設精化前的模型能夠忠實地反映用戶需求,但是在模型精化過程中有時會發(fā)生精化后的模型丟失或違反精化前模型中的相關行為。為此,我們首先對精化前模型分析生成抽象測試用例,并從中抽取出能夠表達系統(tǒng)行為變遷的系統(tǒng)行為并表示為系統(tǒng)行為屬性,然后根據(jù)精化后的模型抽取模型精化關系并進一步更新系統(tǒng)屬性,最后使用這些系統(tǒng)行為屬性來驗證精化后的模型是否依然滿足其代表的系統(tǒng)行為,如果不滿足則說明模型間存在不一致行為,可以通過生成的反例路徑找出不一致的位置,修改不一致后,再迭代進行驗證,直到精化后的模型能夠滿足這些系統(tǒng)屬性為止。最后,為了分析本文方法的有效性,選取了三個常用系統(tǒng)(Celebrity、Kettle、 VOBC)進行一致性檢測,為了模擬出現(xiàn)的不一致情況,人為注入不一致,再利用本文所提出的方法進行一致性檢測,實驗結果表明使用本文方法可以有效找出模型精化前后的大多數(shù)不一致行為,從而實現(xiàn)了使用系統(tǒng)行為屬性的方法來檢測模型間的一致性,提高了模型間一致性檢測的有效性。
【關鍵詞】：模型精化 模型檢測 一致性檢測 屬性抽取 線性時序邏輯
【學位授予單位】：華東師范大學
【學位級別】：碩士
【學位授予年份】：2016
【分類號】：TP311.52
【目錄】：

• 摘要6-8
• ABSTRACT8-12
• 第一章 引言12-18
• 1.1 研究背景和意義12-13
• 1.2 國內(nèi)外研究現(xiàn)狀13-14
• 1.3 關鍵問題與技術路線14-15
• 1.4 主要工作與特色之處15-16
• 1.5 本文的組織結構16-18
• 第二章 相關概念介紹18-21
• 2.1 模型檢測18
• 2.2 模型精化18-19
• 2.3 EVENT-B模型19-20
• 2.4 線性時序邏輯(LINEAR TEMPORAL LOGIC,LTL)20
• 2.5 本章小結20-21
• 第三章 模型系統(tǒng)實例21-28
• 3.1 模型系統(tǒng)概述21-22
• 3.2 電燒水壺模型系統(tǒng)22-26
• 3.3 可能出現(xiàn)的不一致26-27
• 3.4 本章小結27-28
• 第四章 模型間一致性檢測方法28-45
• 4.1 基本流程28-29
• 4.2 抽象測試用例生成29-32
• 4.3 系統(tǒng)行為屬性抽取32-37
• 4.4 精化關系抽取37-42
• 4.5 系統(tǒng)行為屬性驗證42-43
• 4.6 本章小結43-45
• 第五章 實驗分析45-49
• 5.1 實驗內(nèi)容45
• 5.2 實驗數(shù)據(jù)與實驗環(huán)境45-47
• 5.3 實驗結果分析47-48
• 5.4 本章小結48-49
• 第六章 總結與展望49-52
• 6.1 本文總結49-50
• 6.2 未來工作展望50-52
• 附錄1 攻讀學位期間發(fā)表的學術論文目錄52-53
• 附錄2 生成的部分線性時序邏輯(LTL)示例53-56
• 參考文獻56-60
• 致謝60-61

【相似文獻】

中國期刊全文數(shù)據(jù)庫 前6條

1 祁方民;;Petri網(wǎng)結點精化及其應用[J];計算機與現(xiàn)代化;2014年07期

2 王云峰 ,龐軍 ,查鳴 ,楊朝暉 ,鄭國梁;精化演算支撐工具的分析[J];計算機應用與軟件;2002年02期

3 劉瑜,張世琨,鄔倫,葉燕林;地理信息系統(tǒng)中的設計模式——以過濾和精化為例[J];北京大學學報(自然科學版);2001年06期

4 熊建;陳曉克;;基于Wiki技術可持續(xù)精化精品課教學平臺[J];福建電腦;2010年12期

5 楊朝暉;王云峰;鄭國梁;;精化演算支撐工具PRT的研究[J];計算機科學;2000年03期

6 ;[J];;年期

中國重要會議論文全文數(shù)據(jù)庫 前5條

1 周鑫;;面對新形勢、樹立新觀念、迎接新挑戰(zhàn)——談企業(yè)職工面對“精化分立、分業(yè)經(jīng)營”新形勢的感想[A];陜西省體制改革研究會2006-2007優(yōu)秀論文集[C];2007年

2 高陽;王敏中;;拉伸矩形梁的精化理論[A];北京力學會第11屆學術年會論文摘要集[C];2005年

3 高陽;王敏中;;橫觀各項同性壓電矩形直梁的精化理論[A];中國力學學會學術大會'2005論文摘要集（下）[C];2005年

4 趙紅麗;范景輝;郭小方;劉廣;陳建平;;CR輔助的基線參數(shù)精化方法研究[A];第十七屆中國遙感大會摘要集[C];2010年

5 江東;王慶賓;王凱;;重力場精化的空間插值方法研究[A];中國測繪學會2010年學術年會論文集[C];2010年

中國重要報紙全文數(shù)據(jù)庫 前10條

1 羅平華;彩虹精化氣霧漆龍頭今日掛牌[N];證券時報;2008年

2 證券時報記者 羅平華;彩虹精化出口收入逆勢增長三成[N];證券時報;2009年

3 證券時報記者 向南;彩虹精化 涉足室內(nèi)環(huán)保業(yè)務[N];證券時報;2010年

4 記者 翟敏;彩虹精化上半年業(yè)績平平 管理層就“巨額訂單”事件致歉[N];上海證券報;2011年

5 記者 王健杰;彩虹精化營收內(nèi)降外增[N];北京商報;2009年

6 中國空空導彈研究院 綜合管理處;精化軍品能力 優(yōu)化民品結構[N];中國航空報;2004年

7 本報通訊員 周善良 記者 李雨農(nóng);精化分立 一所多制[N];中國航空報;2002年

8 武連寅邋蔡軍;淮化精化再次入選國家高新企業(yè)[N];中國化工報;2007年

9 記者 孫燕飚　劉瓊;萬潤精化再上會 日德企業(yè)“鎖喉”難改觀[N];第一財經(jīng)日報;2011年

10 記者 況玉清;彩虹精化虛假陳述案下月開庭[N];北京商報;2012年

中國博士學位論文全文數(shù)據(jù)庫 前4條

1 陳桂芝;解大規(guī)模非對稱矩陣特征問題的一些精化算法[D];大連理工大學;2000年

2 梁紅瑾;并發(fā)程序精化驗證及其應用[D];中國科學技術大學;2014年

3 牛大田;計算大規(guī)模矩陣部分奇異值分解的精化Lanczos型算法[D];大連理工大學;2003年

4 梁坤;高靈敏度GPS接收技術中幾個關鍵問題的研究[D];中國科學院研究生院（國家天文臺）;2008年

中國碩士學位論文全文數(shù)據(jù)庫 前6條

1 錢潔;軌旁系統(tǒng)的形式化建模精化與驗證[D];華東師范大學;2015年

2 劉婷婷;雙層梁的精化理論[D];遼寧科技大學;2015年

3 王玲;模型精化過程中模型間一致性檢測研究[D];華東師范大學;2016年

4 劉穩(wěn);隱式重啟和精化的全局Lanczos方法與塊Lanczos方法[D];南京航空航天大學;2014年

5 付亞軍;面向多主體的基于政策的運行機制研究[D];湖南大學;2009年

6 吳鋼;解大規(guī)模非對稱矩陣特征問題Lanczos方法的兩種精化版本[D];大連理工大學;2001年

，

本文編號：878298