本文關(guān)鍵詞：基于圖轉(zhuǎn)換的關(guān)聯(lián)屬性規(guī)約模型檢測及其支撐平臺研究

  更多相關(guān)文章： 圖轉(zhuǎn)換 模型檢測 關(guān)聯(lián)屬性

【摘要】：圖轉(zhuǎn)換系統(tǒng)廣泛應(yīng)用在軟件建模和分析階段,現(xiàn)有的圖轉(zhuǎn)換系統(tǒng)通常采用命題式時序邏輯(propositional temporal logic)表達待驗證規(guī)約,但是該邏輯無法直接表達建模實體隨時間演化的關(guān)聯(lián)屬性,提出一種輕量級可支持通用圖轉(zhuǎn)換系統(tǒng)中關(guān)聯(lián)屬性規(guī)約的驗證方法,通過引入標記節(jié)點及相關(guān)屬性,將包含相應(yīng)關(guān)聯(lián)屬性的規(guī)約公式等價轉(zhuǎn)換為常規(guī)命題式時序邏輯,從而可以間接支持該類型規(guī)約的驗證。以流行的對象式圖轉(zhuǎn)換模型檢測工具GROOVE為平臺,結(jié)合啟發(fā)案例,通過實驗驗證了所提出方法的可行性。由于引入標記節(jié)點及屬性來完成關(guān)聯(lián)屬性規(guī)約的驗證會帶來額外的狀態(tài)數(shù),加劇狀態(tài)空間爆炸問題,增加系統(tǒng)開銷,應(yīng)用對稱化簡以及層次化技術(shù),優(yōu)化模型結(jié)構(gòu),減少狀態(tài)數(shù),來節(jié)約系統(tǒng)的時間開銷。結(jié)合具體實例,通過實驗對比,展示出對稱化簡以及圖形層次化技術(shù)在圖轉(zhuǎn)換系統(tǒng)的模型檢測中減少狀態(tài)空間的有效性。此外,為提供更好的可用性,采用圖形化編輯框架GEF(Graphic Editing Framework),以及Eclipse插件式架構(gòu),開發(fā)出一個支撐平臺。根據(jù)所提出方法,該平臺可以展示圖轉(zhuǎn)換工具基本界面結(jié)構(gòu),并能夠自動地引入標記節(jié)點及其相應(yīng)屬性來解決關(guān)聯(lián)屬性的驗證難題,從而可支持對該類系統(tǒng)的驗證工作。
【關(guān)鍵詞】：圖轉(zhuǎn)換 模型檢測 關(guān)聯(lián)屬性
【學(xué)位授予單位】：南京航空航天大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2015
【分類號】：TP311.52
【目錄】：

• 摘要4-5
• Abstract5-11
• 注釋表11-12
• 縮略詞12-13
• 第一章 緒論13-17
• 1.1 研究背景13-15
• 1.1.1 模型檢測13
• 1.1.2 圖轉(zhuǎn)換模型檢測13-15
• 1.2 研究內(nèi)容15-16
• 1.3 研究組織結(jié)構(gòu)16-17
• 第二章 基本概念17-24
• 2.1 圖轉(zhuǎn)換綜述17-19
• 2.2 圖轉(zhuǎn)換模型檢測工具GROOVE19-21
• 2.3 時序邏輯21-22
• 2.4 GEF框架綜述22-24
• 第三章 包含關(guān)聯(lián)屬性的規(guī)約驗證24-42
• 3.1 問題描述24-25
• 3.2 解決方法25-30
• 3.3 狀態(tài)空間縮減方法30-35
• 3.3.1 對稱化簡30-32
• 3.3.2 層次式圖轉(zhuǎn)換32-35
• 3.4 驗證結(jié)果35-42
• 3.4.1 示例 1：車站管理系統(tǒng)的模型檢測35-39
• 3.4.2 示例 2：餐廳服務(wù)系統(tǒng)的模型檢測39-42
• 第四章 支撐平臺構(gòu)建42-58
• 4.1 開發(fā)語言及平臺選擇42-43
• 4.2 框架的選擇43
• 4.3 GEF對MVC模式的實現(xiàn)手段43-45
• 4.4 系統(tǒng)整體設(shè)計45-51
• 4.4.1 系統(tǒng)整體需求45-46
• 4.4.2 Model層設(shè)計46-49
• 4.4.3 Control層設(shè)計49-50
• 4.4.4 View層設(shè)計50-51
• 4.5 系統(tǒng)細節(jié)實現(xiàn)51-58
• 4.5.1 規(guī)則的實現(xiàn)51-52
• 4.5.2 屬性欄的實現(xiàn)52-53
• 4.5.3 分頁實現(xiàn)53-54
• 4.5.4 針對包含關(guān)聯(lián)屬性規(guī)約驗證的處理方法54-56
• 4.5.5 測試56-58
• 第五章 總結(jié)58-59
• 參考文獻59-63
• 致謝63-64
• 在學(xué)期間的研究成果及發(fā)表的學(xué)術(shù)論文64

【相似文獻】

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

1 戎玫;張廣泉;;模型檢測新技術(shù)研究[J];計算機科學(xué);2003年05期

2 肖健宇;張德運;鄭衛(wèi)斌;;過程提取用于改善程序模型檢測的可伸縮性[J];西安交通大學(xué)學(xué)報;2006年06期

3 袁志斌;徐正權(quán);王能超;;軟件模型檢測中的抽象[J];計算機科學(xué);2006年07期

4 劉吉鋒;孫吉貴;;基于抽象-驗證-細化范例的軟件模型檢測[J];計算機科學(xué);2006年12期

5 化志章;吳傳孫;揭安全;薛錦云;;軟件模型檢測新技術(shù)研究[J];微計算機信息;2007年36期

6 王飛明;胡元闖;董榮勝;;模型檢測研究進展[J];廣西科學(xué)院學(xué)報;2008年04期

7 鄺宏斌;羅貴明;;并行軟件模型檢測[J];計算機工程;2008年19期

8 何愷鐸;顧明;宋曉宇;李力;李江;;面向源代碼的軟件模型檢測及其實現(xiàn)[J];計算機科學(xué);2009年01期

9 林璇;;模型檢測方法在入侵檢測中的應(yīng)用研究[J];現(xiàn)代計算機(專業(yè)版);2009年02期

10 顧濱兵;;一種軟件模型檢測方法及其原型系統(tǒng)[J];微計算機應(yīng)用;2010年11期

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

1 高靜;曹子寧;;基于空間邏輯和計算樹邏輯的模型檢測[A];2009年中國高校通信類院系學(xué)術(shù)研討會論文集[C];2009年

2 許梅;曹子寧;;基于謂詞μ演算和空間邏輯的模型檢測算法研究[A];2009年中國高校通信類院系學(xué)術(shù)研討會論文集[C];2009年

3 何青;駱翔宇;蘇開樂;;對弈必勝策略的符號化模型檢測[A];2006年全國理論計算機科學(xué)學(xué)術(shù)年會論文集[C];2006年

4 王飛明;胡元闖;董榮勝;;模型檢測中狀態(tài)爆炸及其優(yōu)化策略研究[A];廣西計算機學(xué)會2008年年會論文集[C];2008年

5 陳道喜;張廣泉;陳冬火;;NSPK協(xié)議的Spin模型檢測[A];2008年全國開放式分布與并行計算機學(xué)術(shù)會議論文集(下冊)[C];2008年

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

1 江華;界程演算模型檢測[D];貴州大學(xué);2008年

2 林榮德;移動界程演算及模型檢測應(yīng)用的關(guān)鍵問題研究[D];華南理工大學(xué);2010年

3 劉劍;傳值進程與移動進程的模型檢測方法[D];中國科學(xué)院研究生院（軟件研究所）;2005年

4 劉志鋒;模型檢測中關(guān)鍵技術(shù)的研究及其應(yīng)用[D];南京大學(xué);2011年

5 朱維軍;時間區(qū)間時序邏輯模型檢測：理論、算法及應(yīng)用[D];西安電子科技大學(xué);2011年

6 尹良澤;基于SAT的組合遷移系統(tǒng)模型檢測技術(shù)研究[D];清華大學(xué);2014年

7 陳冬火;超協(xié)調(diào)時序邏輯及其模型檢測方法[D];中國科學(xué)院研究生院（成都計算機應(yīng)用研究所）;2006年

8 田聰;命題投影時序邏輯的判定性、復(fù)雜性、表達性及模型檢測[D];西安電子科技大學(xué);2010年

9 黃宏濤;基于懶惰切片的模型檢測技術(shù)研究[D];哈爾濱工程大學(xué);2012年

10 劉金卓;基于符號化模型檢測的軟件演化過程模型驗證[D];云南大學(xué);2013年

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

1 李永亮;基于DNA計算的CTL模型檢測方法研究[D];鄭州大學(xué);2015年

2 楊樹峰;基于統(tǒng)計模型檢測的無線傳感器網(wǎng)絡(luò)協(xié)議建模與分析[D];鄭州大學(xué);2015年

3 張興興;基于廣義可能性測度的互模擬及CTL不動點語義[D];陜西師范大學(xué);2015年

4 王彬;基于多值模型檢測的SaaS應(yīng)用測試及其自動化研究[D];陜西師范大學(xué);2015年

5 王凱;基于模型檢測多反例對軟件進行調(diào)試[D];電子科技大學(xué);2015年

6 鄧楠軼;基于廣義可能性測度的模型檢測器GPoCheck的設(shè)計與實現(xiàn)[D];陜西師范大學(xué);2015年

7 張恒;多值模型檢測器的研究與實現(xiàn)[D];陜西師范大學(xué);2015年

8 高毅;不同模型檢測下信號并串轉(zhuǎn)換模塊功能建模的研究[D];電子科技大學(xué);2014年

9 崔曉爽;基于GSTE模型檢測的信號并串轉(zhuǎn)換模塊功能驗證的研究[D];電子科技大學(xué);2014年

10 許落汀;基于BDDs的離散實時時態(tài)邏輯RTCTL*的符號化模型檢測及證據(jù)生成[D];華僑大學(xué);2015年

，

本文編號：694606