基于時(shí)間自動(dòng)機(jī)的車車通信移動(dòng)閉塞功能研究與驗(yàn)證
發(fā)布時(shí)間:2021-03-01 08:24
隨著城軌CBTC(Communication Based Train Control,基于通信的列車運(yùn)行控制)信號(hào)系統(tǒng)的發(fā)展以及5G(5th Generation Mobile Networks,第5代移動(dòng)通信網(wǎng)絡(luò))技術(shù)的應(yīng)用,基于車車通信的列車運(yùn)行控制系統(tǒng)研究應(yīng)運(yùn)而生。該系統(tǒng)突破了傳統(tǒng)CBTC系統(tǒng)以地面設(shè)備為核心的列車控制方式,重組系統(tǒng)架構(gòu),優(yōu)化系統(tǒng)功能,以車載設(shè)備為核心實(shí)現(xiàn)移動(dòng)閉塞功能,提高了列車的靈活性與智能性,同時(shí)由于地面設(shè)備的精簡,使得系統(tǒng)間接口得到簡化,控制信息直達(dá)列車,降低了系統(tǒng)反應(yīng)時(shí)間。車載移動(dòng)閉塞功能作為車車通信列控系統(tǒng)的核心功能,其正確性與有效性必須得到保障。形式化驗(yàn)證與仿真測試驗(yàn)證可以對(duì)系統(tǒng)規(guī)范制定的合理性以及系統(tǒng)功能實(shí)現(xiàn)的有效性進(jìn)行驗(yàn)證,可及時(shí)發(fā)現(xiàn)系統(tǒng)開發(fā)過程中可能存在的不安全因素,對(duì)系統(tǒng)的研究和應(yīng)用具有理論價(jià)值與實(shí)踐意義。本文以車車通信列控系統(tǒng)架構(gòu)為基礎(chǔ),重點(diǎn)研究實(shí)現(xiàn)系統(tǒng)車載移動(dòng)閉塞功能的三大主要功能——前車識(shí)別、列車篩選以及車載移動(dòng)授權(quán)生成,采用時(shí)間自動(dòng)機(jī)理論和UPPAAL工具對(duì)上述功能的具體實(shí)現(xiàn)進(jìn)行了形式化描述與驗(yàn)證,并在測試平臺(tái)上完成了測試驗(yàn)證,驗(yàn)證了系...
【文章來源】:蘭州交通大學(xué)甘肅省
【文章頁數(shù)】:73 頁
【學(xué)位級(jí)別】:碩士
【部分圖文】:
CBTC系統(tǒng)子系統(tǒng)間接口圖
基于時(shí)間自動(dòng)機(jī)的車車通信移動(dòng)閉塞功能研究與驗(yàn)證-2-(Vehicle-to-VehicleCommunicationBasedTrainControlsystem)系統(tǒng)應(yīng)運(yùn)而生,以下簡稱VBTC系統(tǒng)。VBTC系統(tǒng)開發(fā)的核心是簡化傳統(tǒng)系統(tǒng)架構(gòu),減少車站及區(qū)間設(shè)備布置,由車載來實(shí)現(xiàn)列控系統(tǒng)的大部分或全部功能,提高車載的自主性與靈活性?傮w來說VBTC系統(tǒng)具有以下優(yōu)勢[3]:(1)建設(shè)投入和全生命周期成本減少。據(jù)資料顯示,VBTC系統(tǒng)可減少約20%的設(shè)備。信號(hào)設(shè)備大多安裝于列車上,維修工作得到簡化且易于線路擴(kuò)建與改造;(2)系統(tǒng)響應(yīng)時(shí)間縮短,性能得到改善。通過列車間直接通信的方式減少了系統(tǒng)間接口,縮短了系統(tǒng)響應(yīng)時(shí)間;(3)有利于互聯(lián)互通的實(shí)施。系統(tǒng)對(duì)地面設(shè)備依賴減輕且車地通信接口減少,更有利于實(shí)現(xiàn)不同制式之間的互聯(lián)互通。圖1.1與圖1.2分別為CBTC系統(tǒng)與VBTC系統(tǒng)的子系統(tǒng)間接口圖。圖1.1CBTC系統(tǒng)子系統(tǒng)間接口圖圖1.2VBTC系統(tǒng)子系統(tǒng)間接口圖目前對(duì)于VBTC系統(tǒng)的研究尚處于開發(fā)實(shí)驗(yàn)階段,典型的科研單位包括阿爾斯通、交控科技等公司。在一個(gè)新系統(tǒng)的開發(fā)初期,采取一定的方法對(duì)系統(tǒng)進(jìn)行驗(yàn)證是非常有必要的。標(biāo)準(zhǔn)EN50129與IEC61508[4,5]均推薦使用形式化方法對(duì)完善度等級(jí)達(dá)到3級(jí)以上的系統(tǒng)進(jìn)行驗(yàn)證。形式化方法以嚴(yán)格的數(shù)學(xué)定義對(duì)復(fù)雜實(shí)時(shí)系統(tǒng)的功能進(jìn)行描述并建
基于時(shí)間自動(dòng)機(jī)的車車通信移動(dòng)閉塞功能研究與驗(yàn)證-12-(c)E[]p(d)A<>p(e)p→q圖2.1BNF語義示意圖2.4小結(jié)本章對(duì)本課題采用的基礎(chǔ)理論與該理論對(duì)應(yīng)的驗(yàn)證工具進(jìn)行了介紹。首先對(duì)形式化驗(yàn)證方法的概念與特點(diǎn)進(jìn)行了簡要介紹,并對(duì)目前針對(duì)列控系統(tǒng)實(shí)時(shí)性建模驗(yàn)證的形式化方法依據(jù)的數(shù)學(xué)基儲(chǔ)采用的驗(yàn)證工具以及各自的特點(diǎn)進(jìn)行了總結(jié),給出了本文采用時(shí)間自動(dòng)機(jī)作為建模理論的緣由;其次對(duì)時(shí)間自動(dòng)機(jī)理論中的相關(guān)定義與語義進(jìn)行了介紹,并給出了時(shí)間自動(dòng)機(jī)的積的定義;最后對(duì)建模與驗(yàn)證工具UPPAAL的界面組成、使用說明以及驗(yàn)證采用的BNF語法進(jìn)行了介紹。
【參考文獻(xiàn)】:
期刊論文
[1]淺析白盒測試在軟件測試中的應(yīng)用[J]. 田春竹,邢航. 中國信息化. 2019(08)
[2]關(guān)于歐盟Shift2Rail計(jì)劃的研究[J]. 林鴻,王林美,魏艷萍. 國外鐵道車輛. 2019(01)
[3]基于地面無聯(lián)鎖及區(qū)域控制器的新一代CBTC系統(tǒng)方案[J]. 杜恒,孫軍國,張強(qiáng),陳軍. 都市快軌交通. 2017(04)
[4]基于通信的列車控制系統(tǒng)可信構(gòu)造:形式化方法綜述[J]. 陳銘松,鮑勇翔,孫海英,繆煒愷,陳小紅,周庭梁. 軟件學(xué)報(bào). 2017(05)
[5]下一代列控系統(tǒng)技術(shù)方案探討[J]. 程劍鋒,田青,趙顯瓊,孫帝. 中國鐵路. 2014(12)
[6]形式化方法在列車運(yùn)行控制系統(tǒng)中的應(yīng)用[J]. 曹源,唐濤,徐田華,穆建成. 交通運(yùn)輸工程學(xué)報(bào). 2010(01)
[7]基于UPPAAL的鐵路車站信號(hào)聯(lián)鎖系統(tǒng)模型驗(yàn)證[J]. 熊振華,魏臻. 科學(xué)技術(shù)與工程. 2008(07)
[8]仿真系統(tǒng)VV&A及其標(biāo)準(zhǔn)/規(guī)范研究[J]. 劉興堂,劉力,孫文. 計(jì)算機(jī)仿真. 2006(03)
博士論文
[1]CBTC聯(lián)鎖系統(tǒng)的形式化建模與驗(yàn)證方法研究[D]. 于瀟.中國鐵道科學(xué)研究院 2017
[2]列控系統(tǒng)需求規(guī)范形式化建模與驗(yàn)證方法研究[D]. 謝雨飛.北京交通大學(xué) 2012
[3]列車運(yùn)行控制系統(tǒng)分層形式化建模與驗(yàn)證分析[D]. 呂繼東.北京交通大學(xué) 2011
碩士論文
[1]以車載為核心的聯(lián)鎖控制建模與驗(yàn)證研究[D]. 鄭偉.北京交通大學(xué) 2019
[2]基于模型的CBTC區(qū)域控制器測試序列自動(dòng)生成方法的研究[D]. 宋爽.蘭州交通大學(xué) 2018
[3]CBTC區(qū)域控制子系統(tǒng)的建模分析與驗(yàn)證[D]. 楊璐.蘭州交通大學(xué) 2018
[4]基于車車通信的列控系統(tǒng)車載子系統(tǒng)建模與實(shí)現(xiàn)[D]. 許鎮(zhèn).北京交通大學(xué) 2018
[5]基于SCADE的CBTC系統(tǒng)移動(dòng)授權(quán)建模與驗(yàn)證[D]. 楊巧.西南交通大學(xué) 2017
[6]基于時(shí)間自動(dòng)機(jī)的列控中心建模與半實(shí)物仿真[D]. 柳楊.北京交通大學(xué) 2017
[7]車—車通信技術(shù)在列控系統(tǒng)車載設(shè)備中的應(yīng)用研究[D]. 王鵬.北京交通大學(xué) 2017
[8]基于TSSM的車車通信系統(tǒng)車載移動(dòng)授權(quán)模塊的建模和驗(yàn)證[D]. 何芊穎.北京交通大學(xué) 2017
[9]基于狀態(tài)機(jī)的車車通信環(huán)境下列車通信協(xié)作研究[D]. 李聰.北京交通大學(xué) 2017
[10]基于資源自主調(diào)配的聯(lián)鎖子系統(tǒng)在車車通信系統(tǒng)中的應(yīng)用[D]. 方思儀.北京交通大學(xué) 2017
本文編號(hào):3057217
【文章來源】:蘭州交通大學(xué)甘肅省
【文章頁數(shù)】:73 頁
【學(xué)位級(jí)別】:碩士
【部分圖文】:
CBTC系統(tǒng)子系統(tǒng)間接口圖
基于時(shí)間自動(dòng)機(jī)的車車通信移動(dòng)閉塞功能研究與驗(yàn)證-2-(Vehicle-to-VehicleCommunicationBasedTrainControlsystem)系統(tǒng)應(yīng)運(yùn)而生,以下簡稱VBTC系統(tǒng)。VBTC系統(tǒng)開發(fā)的核心是簡化傳統(tǒng)系統(tǒng)架構(gòu),減少車站及區(qū)間設(shè)備布置,由車載來實(shí)現(xiàn)列控系統(tǒng)的大部分或全部功能,提高車載的自主性與靈活性?傮w來說VBTC系統(tǒng)具有以下優(yōu)勢[3]:(1)建設(shè)投入和全生命周期成本減少。據(jù)資料顯示,VBTC系統(tǒng)可減少約20%的設(shè)備。信號(hào)設(shè)備大多安裝于列車上,維修工作得到簡化且易于線路擴(kuò)建與改造;(2)系統(tǒng)響應(yīng)時(shí)間縮短,性能得到改善。通過列車間直接通信的方式減少了系統(tǒng)間接口,縮短了系統(tǒng)響應(yīng)時(shí)間;(3)有利于互聯(lián)互通的實(shí)施。系統(tǒng)對(duì)地面設(shè)備依賴減輕且車地通信接口減少,更有利于實(shí)現(xiàn)不同制式之間的互聯(lián)互通。圖1.1與圖1.2分別為CBTC系統(tǒng)與VBTC系統(tǒng)的子系統(tǒng)間接口圖。圖1.1CBTC系統(tǒng)子系統(tǒng)間接口圖圖1.2VBTC系統(tǒng)子系統(tǒng)間接口圖目前對(duì)于VBTC系統(tǒng)的研究尚處于開發(fā)實(shí)驗(yàn)階段,典型的科研單位包括阿爾斯通、交控科技等公司。在一個(gè)新系統(tǒng)的開發(fā)初期,采取一定的方法對(duì)系統(tǒng)進(jìn)行驗(yàn)證是非常有必要的。標(biāo)準(zhǔn)EN50129與IEC61508[4,5]均推薦使用形式化方法對(duì)完善度等級(jí)達(dá)到3級(jí)以上的系統(tǒng)進(jìn)行驗(yàn)證。形式化方法以嚴(yán)格的數(shù)學(xué)定義對(duì)復(fù)雜實(shí)時(shí)系統(tǒng)的功能進(jìn)行描述并建
基于時(shí)間自動(dòng)機(jī)的車車通信移動(dòng)閉塞功能研究與驗(yàn)證-12-(c)E[]p(d)A<>p(e)p→q圖2.1BNF語義示意圖2.4小結(jié)本章對(duì)本課題采用的基礎(chǔ)理論與該理論對(duì)應(yīng)的驗(yàn)證工具進(jìn)行了介紹。首先對(duì)形式化驗(yàn)證方法的概念與特點(diǎn)進(jìn)行了簡要介紹,并對(duì)目前針對(duì)列控系統(tǒng)實(shí)時(shí)性建模驗(yàn)證的形式化方法依據(jù)的數(shù)學(xué)基儲(chǔ)采用的驗(yàn)證工具以及各自的特點(diǎn)進(jìn)行了總結(jié),給出了本文采用時(shí)間自動(dòng)機(jī)作為建模理論的緣由;其次對(duì)時(shí)間自動(dòng)機(jī)理論中的相關(guān)定義與語義進(jìn)行了介紹,并給出了時(shí)間自動(dòng)機(jī)的積的定義;最后對(duì)建模與驗(yàn)證工具UPPAAL的界面組成、使用說明以及驗(yàn)證采用的BNF語法進(jìn)行了介紹。
【參考文獻(xiàn)】:
期刊論文
[1]淺析白盒測試在軟件測試中的應(yīng)用[J]. 田春竹,邢航. 中國信息化. 2019(08)
[2]關(guān)于歐盟Shift2Rail計(jì)劃的研究[J]. 林鴻,王林美,魏艷萍. 國外鐵道車輛. 2019(01)
[3]基于地面無聯(lián)鎖及區(qū)域控制器的新一代CBTC系統(tǒng)方案[J]. 杜恒,孫軍國,張強(qiáng),陳軍. 都市快軌交通. 2017(04)
[4]基于通信的列車控制系統(tǒng)可信構(gòu)造:形式化方法綜述[J]. 陳銘松,鮑勇翔,孫海英,繆煒愷,陳小紅,周庭梁. 軟件學(xué)報(bào). 2017(05)
[5]下一代列控系統(tǒng)技術(shù)方案探討[J]. 程劍鋒,田青,趙顯瓊,孫帝. 中國鐵路. 2014(12)
[6]形式化方法在列車運(yùn)行控制系統(tǒng)中的應(yīng)用[J]. 曹源,唐濤,徐田華,穆建成. 交通運(yùn)輸工程學(xué)報(bào). 2010(01)
[7]基于UPPAAL的鐵路車站信號(hào)聯(lián)鎖系統(tǒng)模型驗(yàn)證[J]. 熊振華,魏臻. 科學(xué)技術(shù)與工程. 2008(07)
[8]仿真系統(tǒng)VV&A及其標(biāo)準(zhǔn)/規(guī)范研究[J]. 劉興堂,劉力,孫文. 計(jì)算機(jī)仿真. 2006(03)
博士論文
[1]CBTC聯(lián)鎖系統(tǒng)的形式化建模與驗(yàn)證方法研究[D]. 于瀟.中國鐵道科學(xué)研究院 2017
[2]列控系統(tǒng)需求規(guī)范形式化建模與驗(yàn)證方法研究[D]. 謝雨飛.北京交通大學(xué) 2012
[3]列車運(yùn)行控制系統(tǒng)分層形式化建模與驗(yàn)證分析[D]. 呂繼東.北京交通大學(xué) 2011
碩士論文
[1]以車載為核心的聯(lián)鎖控制建模與驗(yàn)證研究[D]. 鄭偉.北京交通大學(xué) 2019
[2]基于模型的CBTC區(qū)域控制器測試序列自動(dòng)生成方法的研究[D]. 宋爽.蘭州交通大學(xué) 2018
[3]CBTC區(qū)域控制子系統(tǒng)的建模分析與驗(yàn)證[D]. 楊璐.蘭州交通大學(xué) 2018
[4]基于車車通信的列控系統(tǒng)車載子系統(tǒng)建模與實(shí)現(xiàn)[D]. 許鎮(zhèn).北京交通大學(xué) 2018
[5]基于SCADE的CBTC系統(tǒng)移動(dòng)授權(quán)建模與驗(yàn)證[D]. 楊巧.西南交通大學(xué) 2017
[6]基于時(shí)間自動(dòng)機(jī)的列控中心建模與半實(shí)物仿真[D]. 柳楊.北京交通大學(xué) 2017
[7]車—車通信技術(shù)在列控系統(tǒng)車載設(shè)備中的應(yīng)用研究[D]. 王鵬.北京交通大學(xué) 2017
[8]基于TSSM的車車通信系統(tǒng)車載移動(dòng)授權(quán)模塊的建模和驗(yàn)證[D]. 何芊穎.北京交通大學(xué) 2017
[9]基于狀態(tài)機(jī)的車車通信環(huán)境下列車通信協(xié)作研究[D]. 李聰.北京交通大學(xué) 2017
[10]基于資源自主調(diào)配的聯(lián)鎖子系統(tǒng)在車車通信系統(tǒng)中的應(yīng)用[D]. 方思儀.北京交通大學(xué) 2017
本文編號(hào):3057217
本文鏈接:http://sikaile.net/kejilunwen/daoluqiaoliang/3057217.html
最近更新
教材專著