列車運(yùn)行控制系統(tǒng)具有分布、動態(tài)、多場景融合等特點(diǎn),系統(tǒng)缺陷在開發(fā)階段難以完全消除。因此,需要在系統(tǒng)部署后實(shí)施運(yùn)行時(shí)監(jiān)控,在發(fā)生危險(xiǎn)時(shí)將系統(tǒng)導(dǎo)向安全側(cè)。運(yùn)行時(shí)驗(yàn)證方法利用形式化語言描述系統(tǒng)期望滿足的監(jiān)控規(guī)約,并通過監(jiān)控器驗(yàn)證系統(tǒng)當(dāng)前的運(yùn)行軌跡是否滿足監(jiān)控規(guī)約,從而實(shí)施運(yùn)行時(shí)監(jiān)控。超速防護(hù)功能的監(jiān)控規(guī)約既包含復(fù)雜的混成行為又高度依賴于列車的運(yùn)行環(huán)境,目前傳統(tǒng)的運(yùn)行時(shí)驗(yàn)證方法難以構(gòu)建有效的監(jiān)控規(guī)約。所以,對超速防護(hù)功能的監(jiān)控規(guī)約構(gòu)建方法的研究十分重要。論文主要工作包含以下四個(gè)方面:（1）提出超速防護(hù)動態(tài)監(jiān)控規(guī)約構(gòu)建方法。通過混成自動機(jī)建模語言建立參數(shù)化列車運(yùn)行控制分層模型,計(jì)算模型關(guān)于超速防護(hù)功能頂層安全需求“列車到達(dá)行車許可終點(diǎn),列車速度不大于零”的可達(dá)集。可達(dá)集中滿足安全需求的部分即為超速防護(hù)監(jiān)控規(guī)約。由于可達(dá)集隨著列車每次運(yùn)行軌跡的變化而發(fā)生改變,所以建立的超速防護(hù)監(jiān)控規(guī)約具有動態(tài)性。（2）提出基于深度學(xué)習(xí)結(jié)合樣條回歸的分段速度監(jiān)控曲線計(jì)算算法�；谠撍惴ù罱ㄋ俣缺O(jiān)控曲線計(jì)算平臺,與參數(shù)化列車運(yùn)行控制分層模型實(shí)時(shí)交互,實(shí)現(xiàn)模型中的速度監(jiān)控曲線計(jì)算功能。該方法用以提升針對不同的列車運(yùn)行環(huán)... 

【文章來源】：北京交通大學(xué)北京市 211工程院校 教育部直屬院校

【文章頁數(shù)】：103 頁

【學(xué)位級別】：碩士

【部分圖文】：

圖２－１在線監(jiān)控框架??Ｆｉｇｕｒｅ?２－１?Ｆｒａｍｅｗｏｒｋ?ｏｆ?ｏｎｌｉｎｅ?ｍｏｎｉｔｏｒｉｎｇ??

圖２－２離線監(jiān)控框架??Ｆｉｇｕｒｅ?２－２?Ｆｒａｍｅｗｏｒｋ?ｏｆ?ｏｆｆｌｉｎｅ?ｍｏｎｉｔｏｒｉｎｇ??系統(tǒng)的運(yùn)行是作用在系統(tǒng)狀態(tài)集合上的無窮運(yùn)行軌跡。在任意時(shí)刻，系統(tǒng)運(yùn)行軌跡都是系統(tǒng)無窮執(zhí)行軌跡的一個(gè)有窮前綴。運(yùn)行時(shí)驗(yàn)證方法是監(jiān)控有窮前綴是否滿足監(jiān)控規(guī)約，給出監(jiān)控結(jié)果。然而，對系統(tǒng)的有窮前綴的判是否同樣適用于系統(tǒng)以該有窮前綴實(shí)際運(yùn)行的無窮運(yùn)行軌跡，所以需要找的有窮前綴與無窮運(yùn)行軌跡的相互關(guān)系。另外，在在線監(jiān)控中，發(fā)現(xiàn)系統(tǒng)危固然重要，如果監(jiān)控器可以盡可能早的發(fā)現(xiàn)系統(tǒng)危險(xiǎn)狀態(tài)，保證系統(tǒng)安全可更為重要。??Ｍａｒｔｉｎ?Ｌｅｕｃｋｅｒ等人提出了預(yù)測監(jiān)控器需要滿足的兩太性質(zhì)：??公平性：給定一條有窮軌跡，如果存在不同的無窮后綴使得監(jiān)控器判定出監(jiān)控結(jié)果，那么該有窮軌跡應(yīng)該被判定為不確定。??預(yù)測性：給定一條有窮軌跡，對于其所有的無窮后綴，監(jiān)控器都將判定出監(jiān)控結(jié)果，那么該有窮軌跡也將被判定為相同的監(jiān)控結(jié)果。??

?Ｉ?監(jiān)控結(jié)果??圖２－２離線監(jiān)控框架??Ｆｉｇｕｒｅ?２－２?Ｆｒａｍｅｗｏｒｋ?ｏｆ?ｏｆｆｌｉｎｅ?ｍｏｎｉｔｏｒｉｎｇ??系統(tǒng)的運(yùn)行是作用在系統(tǒng)狀態(tài)集合上的無窮運(yùn)行軌跡。在任意時(shí)刻，系統(tǒng)當(dāng)前??的運(yùn)行軌跡都是系統(tǒng)無窮執(zhí)行軌跡的一個(gè)有窮前綴。運(yùn)行時(shí)驗(yàn)證方法是監(jiān)控系統(tǒng)??的有窮前綴是否滿足監(jiān)控規(guī)約，給出監(jiān)控結(jié)果。然而，對系統(tǒng)的有窮前綴的判定結(jié)??果是否同樣適用于系統(tǒng)以該有窮前綴實(shí)際運(yùn)行的無窮運(yùn)行軌跡，所以需要找出系??統(tǒng)的有窮前綴與無窮運(yùn)行軌跡的相互關(guān)系。另外，在在線監(jiān)控中，發(fā)現(xiàn)系統(tǒng)危險(xiǎn)狀??態(tài)固然重要，如果監(jiān)控器可以盡可能早的發(fā)現(xiàn)系統(tǒng)危險(xiǎn)狀態(tài)，保證系統(tǒng)安全可靠運(yùn)??行更為重要。??Ｍａｒｔｉｎ?Ｌｅｕｃｋｅｒ等人提出了預(yù)測監(jiān)控器需要滿足的兩太性質(zhì)：??公平性：給定一條有窮軌跡，如果存在不同的無窮后綴使得監(jiān)控器判定出不同??的監(jiān)控結(jié)果，那么該有窮軌跡應(yīng)該被判定為不確定。??預(yù)測性：給定一條有窮軌跡

【參考文獻(xiàn)】：
期刊論文
[1]參數(shù)化運(yùn)行時(shí)驗(yàn)證研究和工具實(shí)現(xiàn)[J]. 王哲民,陳哲,朱云龍,黃志球.  小型微型計(jì)算機(jī)系統(tǒng). 2016(12)
[2]基于時(shí)間屬性序列圖的監(jiān)控器構(gòu)造方法[J]. 葉俊民,辜劍,陳曙,董威,舒紹嫻.  小型微型計(jì)算機(jī)系統(tǒng). 2015(07)
[3]列控設(shè)備動態(tài)監(jiān)測系統(tǒng)的深度應(yīng)用[J]. 王東.  鐵道通信信號. 2014(11)
[4]一種運(yùn)行時(shí)驗(yàn)證監(jiān)控器的構(gòu)造方法[J]. 張可迪,董威.  計(jì)算機(jī)光盤軟件與應(yīng)用. 2012(20)
[5]一種基于CPN的運(yùn)行時(shí)監(jiān)控服務(wù)交互行為的方法[J]. 朱俊,郭長國,吳泉源.  計(jì)算機(jī)研究與發(fā)展. 2011(12)
[6]運(yùn)行時(shí)驗(yàn)證及其在列車運(yùn)行控制系統(tǒng)中的應(yīng)用[J]. 趙林,唐濤,徐田華,柴銘,李憲.  鐵道學(xué)報(bào). 2011(12)
[7]面向參數(shù)化LTL的預(yù)測監(jiān)控器構(gòu)造技術(shù)[J]. 趙常智,董威,隋平,齊治昌.  軟件學(xué)報(bào). 2010(02)

博士論文
[1]基于AOP的軟件運(yùn)行時(shí)驗(yàn)證關(guān)鍵技術(shù)研究[D]. 張獻(xiàn).國防科學(xué)技術(shù)大學(xué) 2012

碩士論文
[1]基于公式重寫的實(shí)時(shí)時(shí)序約束驗(yàn)證及其在列控背景下的應(yīng)用[D]. 李旸.北京交通大學(xué) 2015
[2]面向列控安全性監(jiān)控的運(yùn)行時(shí)驗(yàn)證方法研究[D]. 徐蛟.國防科學(xué)技術(shù)大學(xué) 2014



本文編號：3601143