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

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

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

【學位級別】：碩士

【部分圖文】：

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

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

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

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

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

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



本文編號：3601143