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

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

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

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