面向列控安全性監(jiān)控的運行時驗證方法研究.pdf

1、列車控制系統(tǒng)是軌道交通信號系統(tǒng)的重要組成部分之一，是保證列車運行安全的重要部分，測試與形式驗證是確保其安全性的主要途徑。傳統(tǒng)的測試方式由于其不完備性，難以測試可能的運行環(huán)境與路徑，因此無法保證運行后的系統(tǒng)不存在安全缺陷；模型檢驗是一種完備的驗證系統(tǒng)的方法，但是會遇到模型刻畫能力與驗證能力矛盾的問題，尤其是狀態(tài)爆炸問題會使得該方法對于復(fù)雜系統(tǒng)難以適用。運行時驗證是一種輕量級的驗證技術(shù)，其驗證過程伴隨目標系統(tǒng)的實際運行，對系統(tǒng)運行路徑是否滿

2、足安全性質(zhì)進行及時監(jiān)控，是傳統(tǒng)測試和驗證技術(shù)的有效補充，在許多領(lǐng)域逐漸受到人們的關(guān)注，并被具體運用到眾多對系統(tǒng)安全性有著較高要求的行業(yè)。
　　本文針對列控系統(tǒng)中分路不良、無線閉塞中心RBC切換等對列控安全極其重要的問題入手，研究相應(yīng)的運行時驗證技術(shù)，包括：
　?。?）分析軌道電路子系統(tǒng)中分路不良場景及其發(fā)生的原因，總結(jié)了對分路不良進行監(jiān)控以保證列車安全性的一組關(guān)鍵性質(zhì)，并提出用線性時序邏輯（LTL）描述和生成監(jiān)控器的方法。由

3、于分路不良問題需要多個監(jiān)控監(jiān)控器同時監(jiān)控，為了提高監(jiān)控效率，還提出了了針對分路不良的多監(jiān)控器調(diào)度策略。
　　（2）為了實現(xiàn)監(jiān)控性質(zhì)的輔助描述和自動生成，本文針對列控系統(tǒng)安全性監(jiān)控需要考慮的主要特征，包括監(jiān)控事件的描述、非插裝式的監(jiān)控器運行機制、列控系統(tǒng)主要采用C語言等，對JavaMOP監(jiān)控工具進行擴展，對其MOP文件格式重新設(shè)計，擴展了事件與條件定義語言，并實現(xiàn)了相應(yīng)的監(jiān)控器生成工具。
　　（3）為了驗證上述方法和工具的有效