本文關(guān)鍵詞：基于模型檢測的軌道交通運營場景安全性分析

  更多相關(guān)文章： 模型檢測 UPPAAL工具 時間自動機 可達(dá)性分析

【摘要】：軌道交通這樣的實時系統(tǒng)對時間的要求及其嚴(yán)格,要保障軌道交通運營場景的安全性,就需要對運營場景進(jìn)行安全檢測,而保證系統(tǒng)安全性的關(guān)鍵任務(wù)就是實時系統(tǒng)的時間約束的滿足性。針對此問題,模型檢測技術(shù)得以應(yīng)用,模型檢測的原理是為系統(tǒng)建立模型,用時態(tài)邏輯表示需要檢測的性質(zhì),然后用檢測算法檢測該模型是否滿足性質(zhì)。使用的檢測工具是UPPAAL工具,根據(jù)檢測步驟需要理解UPPAAL工具的模型時間自動機的構(gòu)造及如何用規(guī)范語言表示性質(zhì),還要理解其檢測算法的實現(xiàn)。本文針對軌道交通的運營場景之一的RBC切換場景進(jìn)行驗證,使用UPPAAL工具驗證其切換過程中的安全性。對實時系統(tǒng)的絕大多數(shù)安全性和活性的檢測,模型檢測都是通過可達(dá)性分析算法來完成�？蛇_(dá)性分析算法是模型檢測的基礎(chǔ),由于時間自動機的時間約束而加速了狀態(tài)空間爆炸,增加了可達(dá)性分析算法的復(fù)雜性。已存的時間自動機可達(dá)性分析算法,或是基于等價時間區(qū)域圖(Region)、有界差分矩陣DBM)采用半符號時間約束結(jié)構(gòu)的狀態(tài)空間遍歷分析方法；或是基于BDD結(jié)構(gòu)采用全符號時間約束的狀態(tài)空間遍歷方法。這兩類方法割裂了狀態(tài)變遷表達(dá)與時間約束表達(dá)符號關(guān)聯(lián),難以應(yīng)用大規(guī)模案例分析。本文的主要工作是：1)采用常用的檢測工具是UPPAAL工具,對典型的軌道交通運營場景進(jìn)行功能安全性和時間約束的安全性進(jìn)行檢測,從而能夠?qū)崿F(xiàn)系統(tǒng)模型的安全性分析。2)提出一種全符號的可達(dá)性分析方法,采用BDD結(jié)構(gòu)統(tǒng)一表達(dá)時間自動機的狀態(tài)變遷空間和時間約束,給出了在狀態(tài)可達(dá)全符號運算的基礎(chǔ)上時間約束的運算系列算法,并給出了單自動機、多自動機的可達(dá)算法。最后實例驗證算法的正確性。通過這種方法,可以實現(xiàn)時間自動機的全符號化可達(dá)性分析,為全符號時間系統(tǒng)模型檢測提供分析基礎(chǔ)。
【關(guān)鍵詞】：模型檢測 UPPAAL工具 時間自動機 可達(dá)性分析
【學(xué)位授予單位】：青島科技大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2015
【分類號】：U298
【目錄】：

• 摘要3-4
• ABSTRACT4-8
• 1 前言8-13
• 1.1 研究背景和意義8-9
• 1.2 研究現(xiàn)狀9-10
• 1.3 主要研究內(nèi)容10-13
• 2 系統(tǒng)建模13-25
• 2.1 模型檢測的介紹13-14
• 2.2 統(tǒng)一建模語言UML順序圖14-16
• 2.2.1 UML介紹14
• 2.2.2 UML順序圖14-15
• 2.2.3 UML順序圖的擴展15-16
• 2.3 實現(xiàn)工具UPPAAL16-20
• 2.3.1 UPPAAL介紹16-17
• 2.3.2 UPPAAL的檢測步驟17-19
• 2.3.3 UPPAAL的檢測語法19-20
• 2.4 時間自動機模型的理論基礎(chǔ)20-23
• 2.4.1 有時間約束的轉(zhuǎn)換系統(tǒng)20-21
• 2.4.2 時間自動機的語法和語義21
• 2.4.3 時間自動機積的構(gòu)造21-23
• 2.5 UML順序圖到時間自動機模型的轉(zhuǎn)換23-25
• 3 系統(tǒng)性質(zhì)25-32
• 3.1 計算樹時態(tài)邏輯CTL*25-27
• 3.2 CTL和LTL27-30
• 3.2.1 LTL27-28
• 3.2.2 CTL28-30
• 3.3 CTL和LTL的模型檢測算法30-32
• 3.3.1 CTL的模型檢測算法30
• 3.3.2 LTL的模型檢測算法30-32
• 4 運營場景的安全驗證32-45
• 4.1 CTCS-3級列控系統(tǒng)簡介32
• 4.2 CTCS-3運營場景之RBC切換32-34
• 4.3 RBC切換場景的建模34-43
• 4.3.1 建立RBC切換場景的UML模型34-37
• 4.3.2 建立RBC切換場景的UPPAAL模型-時間自動機網(wǎng)絡(luò)37-43
• 4.4 RBC切換場景的安全驗證分析43-45
• 5 基于BDD的全符號化的可達(dá)性算法45-72
• 5.1 已有的半符號化可達(dá)性分析方法45-49
• 5.1.1 域自動機45-46
• 5.1.2 帶自動機46-49
• 5.2 基于BDD的全符號化可達(dá)性算法49-63
• 5.2.1 BDD存儲結(jié)構(gòu)理論49-53
• 5.2.2 一種時間約束的BDD存儲結(jié)構(gòu)——DDD結(jié)構(gòu)53-59
• 5.2.3 單時間自動機的可達(dá)性分析算法59-60
• 5.2.4 多時間自動機的可達(dá)性分析算法60-63
• 5.3 全符號化的可達(dá)性分析算法實例63-72
• 總結(jié)與展望72-73
• 參考文獻(xiàn)73-77
• 致謝77-78
• 攻讀學(xué)位期間發(fā)表的學(xué)術(shù)論文目錄78
• 攻讀學(xué)位期間參加的科研項目78-79

【相似文獻(xiàn)】

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

1 梅元媛;;使用模型檢測器進(jìn)行測試的方法研究[J];廣西輕工業(yè);2007年02期

2 陸公正,戎玫,張廣泉;基于稠密時間的實時系統(tǒng)模型檢測的一個應(yīng)用[J];蘇州大學(xué)學(xué)報(工科版);2005年02期

3 方憶湘;高婷;黃風(fēng)山;;Pro/E環(huán)境下零件MBD模型檢測信息的獲取[J];組合機床與自動化加工技術(shù);2013年09期

4 ;[J];;年期

中國重要會議論文全文數(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 劉劍;傳值進(jìn)程與移動進(jìn)程的模型檢測方法[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á)性及模型檢測[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 王凱;基于模型檢測多反例對軟件進(jìn)行調(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年

，

本文編號：712983