本文關(guān)鍵詞：基于模型檢測(cè)的軌道交通運(yùn)營(yíng)場(chǎng)景安全性分析

  更多相關(guān)文章： 模型檢測(cè) UPPAAL工具 時(shí)間自動(dòng)機(jī) 可達(dá)性分析

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

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

【相似文獻(xiàn)】

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

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

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

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

4 ;[J];;年期

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

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

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

3 何青;駱翔宇;蘇開樂(lè);;對(duì)弈必勝策略的符號(hào)化模型檢測(cè)[A];2006年全國(guó)理論計(jì)算機(jī)科學(xué)學(xué)術(shù)年會(huì)論文集[C];2006年

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

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

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

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

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

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

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

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

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

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

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

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

10 劉金卓;基于符號(hào)化模型檢測(cè)的軟件演化過(guò)程模型驗(yàn)證[D];云南大學(xué);2013年

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

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

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

3 張興興;基于廣義可能性測(cè)度的互模擬及CTL不動(dòng)點(diǎn)語(yǔ)義[D];陜西師范大學(xué);2015年

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

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

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

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

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

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

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

，

本文編號(hào)：712983