本文關(guān)鍵詞：CPS系統(tǒng)動(dòng)態(tài)行為在線建模與驗(yàn)證研究，由筆耕文化傳播整理發(fā)布。

【摘要】：在安全攸關(guān)領(lǐng)域,如航空、航天、列車(chē)控制和醫(yī)療等,信息物理融合系統(tǒng)(Cyber-Physical System,CPS)具有很高的安全需求。在測(cè)試和仿真并不能保證沒(méi)有系統(tǒng)錯(cuò)誤的情況下,如何通過(guò)形式化建模與驗(yàn)證的方法保證系統(tǒng)安全是相關(guān)領(lǐng)域的重點(diǎn)關(guān)注問(wèn)題。在動(dòng)態(tài)實(shí)時(shí)的CPS系統(tǒng)中大量實(shí)時(shí)參數(shù)信息的存在會(huì)導(dǎo)致?tīng)顟B(tài)空間難以準(zhǔn)確表示,從而使得傳統(tǒng)的靜態(tài)模型檢驗(yàn)難以進(jìn)行。針對(duì)此問(wèn)題,相關(guān)學(xué)者提出了CPS系統(tǒng)在線建模與驗(yàn)證的方法,即利用參數(shù)信息在系統(tǒng)實(shí)際運(yùn)轉(zhuǎn)過(guò)程中不斷更新且可獲取這一特點(diǎn),針對(duì)短時(shí)間周期內(nèi)的系統(tǒng)行為建立模型并周期性驗(yàn)證。然而,在對(duì)列車(chē)控制系統(tǒng)這個(gè)典型的CPS系統(tǒng)的分析過(guò)程中,本文指出在實(shí)際的CPS系統(tǒng)上應(yīng)用在線驗(yàn)證存在兩方面的問(wèn)題。一方面,傳統(tǒng)的流水線式的設(shè)計(jì)會(huì)存在的驗(yàn)證不能完全覆蓋系統(tǒng)行為的問(wèn)題,同時(shí)傳統(tǒng)的設(shè)計(jì)中并沒(méi)有考慮驗(yàn)證的時(shí)效性問(wèn)題；另一方面,實(shí)際的列車(chē)車(chē)載設(shè)備計(jì)算能力有限,在線驗(yàn)證面臨多車(chē)多任務(wù)等因素帶來(lái)的效率問(wèn)題。為了解決以上兩個(gè)問(wèn)題,確保在線驗(yàn)證的可靠性和高效性,本文的主要工作如下：1.提出了一種多機(jī)制觸發(fā)下面向全周期覆蓋的在線驗(yàn)證方法。以列控系統(tǒng)為例分析了流水線式在線驗(yàn)證過(guò)程中存在的覆蓋問(wèn)題和時(shí)效性問(wèn)題,對(duì)在線驗(yàn)證設(shè)計(jì)過(guò)程中的幾個(gè)重要參數(shù)進(jìn)行了討論,提出了一系列在線驗(yàn)證設(shè)計(jì)應(yīng)滿足的參數(shù)規(guī)約,在對(duì)驗(yàn)證規(guī)約進(jìn)行了理論分析后,給出了在參數(shù)規(guī)約的指導(dǎo)下設(shè)計(jì)的多機(jī)制觸發(fā)下面向全周期覆蓋的設(shè)計(jì)方法,針對(duì)所提出方法我們?cè)O(shè)計(jì)了三組場(chǎng)景實(shí)驗(yàn),從場(chǎng)景分析的角度說(shuō)明了方法的必要性和正確性。2.提出了一種分布式的在線驗(yàn)證設(shè)計(jì)框架。通過(guò)對(duì)Linux Virtual Server技術(shù)思想的分析,從伸縮性、可靠性和透明性的角度出發(fā),結(jié)合在線驗(yàn)證本身的特點(diǎn),設(shè)計(jì)了一種在線驗(yàn)證的分布式框架,該框架包含任務(wù)配置模塊,負(fù)載調(diào)度模塊,后臺(tái)驗(yàn)證模塊和共享存儲(chǔ)區(qū)。在我們提出的框架設(shè)計(jì)的基礎(chǔ)上搭建了進(jìn)行了分布式在線驗(yàn)證云平臺(tái),并在云平臺(tái)上進(jìn)行了效率實(shí)驗(yàn)。3.與北京交通大學(xué)合作,在其軌道交通運(yùn)行控制系統(tǒng)國(guó)家工程研究中心的北京亦莊線CBTC仿真測(cè)試子平臺(tái)上進(jìn)行了在線驗(yàn)證模塊的設(shè)計(jì)與部署。通過(guò)對(duì)平臺(tái)上亦莊線列車(chē)控制機(jī)制的分析建立了形式化模型,統(tǒng)一了車(chē)載設(shè)備接口信息并對(duì)實(shí)時(shí)參數(shù)進(jìn)行了區(qū)段換算、曲線計(jì)算等一系列處理,對(duì)驗(yàn)證工具SpaceEx進(jìn)行包裝使其成為周期型驗(yàn)證后臺(tái),將在線驗(yàn)證模塊部署在仿真平臺(tái)的控制臺(tái)上后設(shè)計(jì)了場(chǎng)景實(shí)驗(yàn),證明了在線驗(yàn)證在實(shí)際的CPS系統(tǒng)上的有效性。
【關(guān)鍵詞】：信息物理融合系統(tǒng) 列控系統(tǒng) 在線建模與驗(yàn)證 分布式框架 亦莊線實(shí)例研究
【學(xué)位授予單位】：南京大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2016
【分類(lèi)號(hào)】：TP311.52
【目錄】：

• 摘要4-6
• Abstract6-14
• 第一章 緒論14-24
• 1.1 研究背景14-16
• 1.1.1 信息物理融合系統(tǒng)14-15
• 1.1.2 軟件系統(tǒng)質(zhì)量保證15-16
• 1.2 研究現(xiàn)狀16-21
• 1.2.1 CPS系統(tǒng)安全保障現(xiàn)狀16-17
• 1.2.2 形式化方法與模型檢驗(yàn)17-19
• 1.2.3 混成系統(tǒng)與可達(dá)性驗(yàn)證19-20
• 1.2.4 CPS系統(tǒng)在線驗(yàn)證20-21
• 1.3 本文工作21-22
• 1.3.1 多機(jī)制觸發(fā)全覆蓋在線驗(yàn)證21-22
• 1.3.2 分布式在線驗(yàn)證框架22
• 1.3.3 亦莊線實(shí)例研究22
• 1.4 論文結(jié)構(gòu)安排22-24
• 第二章 背景知識(shí)與理論基礎(chǔ)24-32
• 2.1 CPS系統(tǒng)與列控系統(tǒng)24-26
• 2.1.1 CPS系統(tǒng)與實(shí)時(shí)系統(tǒng)24-25
• 2.1.2 列車(chē)控制系統(tǒng)25-26
• 2.2 混成系統(tǒng)和混成自動(dòng)機(jī)26-28
• 2.3 CPS系統(tǒng)在線驗(yàn)證與流水線式設(shè)計(jì)28-30
• 2.3.1 在線驗(yàn)證28-29
• 2.3.2 流水線式設(shè)計(jì)29-30
• 2.4 本章小結(jié)30-32
• 第三章 多機(jī)制觸發(fā)下面向全周期覆蓋的在線驗(yàn)證32-52
• 3.1 問(wèn)題分析32-36
• 3.1.1 覆蓋性問(wèn)題32-35
• 3.1.2 時(shí)效性問(wèn)題35-36
• 3.2 多機(jī)制觸發(fā)下面向全周期覆蓋的在線驗(yàn)證方法36-43
• 3.2.1 在線驗(yàn)證過(guò)程中關(guān)鍵參數(shù)36-39
• 3.2.2 參數(shù)規(guī)約及分析39-42
• 3.2.3 多機(jī)制觸發(fā)下在線驗(yàn)證方法42-43
• 3.3 實(shí)驗(yàn)研究43-50
• 3.3.1 建模43-45
• 3.3.2 場(chǎng)景分析45-50
• 3.4 本章小結(jié)50-52
• 第四章 分布式在線驗(yàn)證52-68
• 4.1 問(wèn)題分析52-55
• 4.2 基于LVS框架的分布式在線驗(yàn)證設(shè)計(jì)55-58
• 4.2.1 Linux Virtual Server集群技術(shù)55-56
• 4.2.2 分布式在線驗(yàn)證框架設(shè)計(jì)56-58
• 4.3 關(guān)鍵技術(shù)解決方案58-64
• 4.3.1 共享存儲(chǔ)區(qū)設(shè)計(jì)58-61
• 4.3.2 負(fù)載調(diào)度模塊設(shè)計(jì)61-64
• 4.4 平臺(tái)實(shí)現(xiàn)及實(shí)驗(yàn)研究64-66
• 4.5 本章小結(jié)66-68
• 第五章 亦莊線實(shí)例研究68-82
• 5.1 平臺(tái)介紹68-72
• 5.2 平臺(tái)設(shè)計(jì)與實(shí)現(xiàn)72-78
• 5.2.1 總體設(shè)計(jì)72
• 5.2.2 建模72-75
• 5.2.3 數(shù)據(jù)處理75-77
• 5.2.4 驗(yàn)證工具及傳輸設(shè)計(jì)77-78
• 5.3 實(shí)驗(yàn)結(jié)果78-80
• 5.4 本章小結(jié)80-82
• 第六章 總結(jié)與展望82-86
• 6.1 論文的主要工作82-83
• 6.2 未來(lái)工作83-86
• 參考文獻(xiàn)86-92
• 附錄92-94
• 簡(jiǎn)歷與科研成果94-96
• 致謝96-97

【相似文獻(xiàn)】

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

1 周小輝;;基于列控系統(tǒng)車(chē)——地間信息傳輸方式的研究[J];甘肅科技縱橫;2007年01期

2 楊絢;陳德旺;陳榮;;高速鐵路列控系統(tǒng)主動(dòng)安全控制的分析與思考[J];鐵路計(jì)算機(jī)應(yīng)用;2012年08期

3 楊永清;郜春海;王海峰;;基于XML列控系統(tǒng)數(shù)據(jù)模型建立[J];鐵路計(jì)算機(jī)應(yīng)用;2011年11期

4 何浩洋;穆建成;馬連川;曹源;;改進(jìn)FlexRay總線的設(shè)計(jì)與實(shí)現(xiàn)[J];鐵路計(jì)算機(jī)應(yīng)用;2013年04期

5 王云珠;陳邦興;;故障樹(shù)分析法在C3列控系統(tǒng)風(fēng)險(xiǎn)分析中的應(yīng)用[J];信息技術(shù);2009年10期

6 張瑋;;GSM-R在高速鐵路列控系統(tǒng)中的應(yīng)用方案探討[J];通信技術(shù);2009年05期

7 呂繼東;唐濤;;高速鐵路列控系統(tǒng)運(yùn)營(yíng)場(chǎng)景實(shí)時(shí)性的建模與驗(yàn)證[J];鐵道學(xué)報(bào);2011年06期

8 鐘強(qiáng);;動(dòng)車(chē)事故發(fā)生在“仲夏”嗎[J];咬文嚼字;2011年12期

9 趙林;唐濤;劉金濤;劉超;李憲;;基于UML擴(kuò)展機(jī)制的列控系統(tǒng)建模方法研究[J];鐵道學(xué)報(bào);2012年12期

10 鄭升;曹源;張玉琢;景浩;胡華;;通用型列控系統(tǒng)的安全計(jì)算機(jī)設(shè)計(jì)與驗(yàn)證[J];北京交通大學(xué)學(xué)報(bào);2014年03期

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

1 管建華;王海忠;;高速客運(yùn)專(zhuān)線列控系統(tǒng)方案的思考[A];鐵路客運(yùn)專(zhuān)線建設(shè)技術(shù)交流會(huì)論文集[C];2005年

2 范麗君;;秦沈線TVM430系統(tǒng)點(diǎn)式功能的探討[A];鐵道科學(xué)技術(shù)新進(jìn)展——鐵道科學(xué)研究院五十五周年論文集[C];2005年

3 呂書(shū)麗;;列控系統(tǒng)車(chē)載設(shè)備發(fā)展淺談[A];科技、工程與經(jīng)濟(jì)社會(huì)協(xié)調(diào)發(fā)展——中國(guó)科協(xié)第五屆青年學(xué)術(shù)年會(huì)論文集[C];2004年

4 呂書(shū)麗;;列控系統(tǒng)車(chē)載設(shè)備發(fā)展淺談[A];快速提升鐵路建設(shè)與裝備現(xiàn)代化技術(shù)促進(jìn)鐵路跨越式發(fā)展——中國(guó)科協(xié)第五屆青年學(xué)術(shù)年會(huì)第九分會(huì)場(chǎng)論文集[C];2004年

中國(guó)重要報(bào)紙全文數(shù)據(jù)庫(kù) 前4條

1 本報(bào)特約記者 楊光和;C3之光照亮絢麗人生[N];人民鐵道;2010年

2 記者 張麗華　李娟;鐵道部徹查列控系統(tǒng) 直指“通號(hào)系”[N];第一財(cái)經(jīng)日?qǐng)?bào);2011年

3 本報(bào)記者 宋菁;廣深港高鐵全面檢測(cè)列控系統(tǒng)[N];21世紀(jì)經(jīng)濟(jì)報(bào)道;2011年

4 邵文杰;信號(hào)控制技術(shù)具有自主知識(shí)產(chǎn)權(quán)[N];光明日?qǐng)?bào);2007年

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

1 謝雨飛;列控系統(tǒng)需求規(guī)范形式化建模與驗(yàn)證方法研究[D];北京交通大學(xué);2012年

2 呂繼東;列車(chē)運(yùn)行控制系統(tǒng)分層形式化建模與驗(yàn)證分析[D];北京交通大學(xué);2011年

3 譚平;城際鐵路車(chē)載列控系統(tǒng)安全及智能控制關(guān)鍵技術(shù)研究[D];浙江大學(xué);2014年

4 蔡伯根;低成本列控系統(tǒng)的列車(chē)組合定位理論與方法[D];北京交通大學(xué);2010年

5 曹源;高速鐵路列車(chē)運(yùn)行控制系統(tǒng)的形式化建模與驗(yàn)證方法研究[D];北京交通大學(xué);2011年

6 張亞?wèn)|;高速鐵路列車(chē)運(yùn)行控制系統(tǒng)安全風(fēng)險(xiǎn)辨識(shí)及分析研究[D];西南交通大學(xué);2013年

7 邢小琴;高速鐵路GSM-R網(wǎng)絡(luò)檢測(cè)/監(jiān)測(cè)數(shù)據(jù)分析關(guān)鍵技術(shù)研究[D];中國(guó)鐵道科學(xué)研究院;2014年

8 劉金濤;基于STPA的需求階段的高速列車(chē)運(yùn)行控制系統(tǒng)安全分析方法研究[D];北京交通大學(xué);2015年

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

1 程瑞軍;列控系統(tǒng)混成行為的建模與驗(yàn)證方法[D];北京交通大學(xué);2014年

2 袁敏;基于彈復(fù)力的列控系統(tǒng)可靠性實(shí)時(shí)分析方法研究[D];北京交通大學(xué);2016年

3 任鵬程;復(fù)雜場(chǎng)景下列控系統(tǒng)功能驗(yàn)證分析[D];北京交通大學(xué);2016年

4 胡瑞;列控系統(tǒng)地面目標(biāo)控制器的設(shè)計(jì)與實(shí)現(xiàn)[D];北京交通大學(xué);2016年

5 劉潤(rùn);CPS系統(tǒng)動(dòng)態(tài)行為在線建模與驗(yàn)證研究[D];南京大學(xué);2016年

6 夏青;列控系統(tǒng)數(shù)字軌道地圖生成算法研究[D];蘭州交通大學(xué);2012年

7 程雨;基于貝葉斯網(wǎng)絡(luò)的列控系統(tǒng)故障診斷研究[D];北京交通大學(xué);2014年

8 衛(wèi)建芳;基于高速鐵路列控系統(tǒng)通信協(xié)議的研究與應(yīng)用[D];西安電子科技大學(xué);2011年

9 趙晶晶;基于模糊貝葉斯網(wǎng)絡(luò)的故障診斷方法研究及其在列控系統(tǒng)中的應(yīng)用[D];北京交通大學(xué);2013年

10 高僮;基于動(dòng)態(tài)故障樹(shù)和蒙特卡洛仿真的列控系統(tǒng)風(fēng)險(xiǎn)分析研究[D];北京交通大學(xué);2014年

  本文關(guān)鍵詞：CPS系統(tǒng)動(dòng)態(tài)行為在線建模與驗(yàn)證研究，由筆耕文化傳播整理發(fā)布。

，

本文編號(hào)：463399