軌道交通車載控制器實時時序行為的監(jiān)控方法研究.pdf

1、軌道交通是我國交通體系中的一個重要組成部分，隨著軌道交通的日益完善，功能系統(tǒng)日益復雜，安全問題也不斷突出。列車運行控制系統(tǒng)作為軌道交通中的一個重要系統(tǒng)，也是集控制、通信、計算和信號于一體的復雜系統(tǒng)?，F(xiàn)階段對列車運行控制系統(tǒng)安全驗證的傳統(tǒng)測試和驗證方法都有其局限性，而運行時驗證方法是結(jié)合了傳統(tǒng)測試和模型檢驗方法的輕量級形式化方法。它有效降低了對安全苛求的列車運行控制系統(tǒng)安全驗證的復雜度，同時提高了驗證的效率。目前對運行時驗證研究比較多的是

2、線性時序邏輯(LTL)，但LTL只能對系統(tǒng)執(zhí)行的狀態(tài)序列進行監(jiān)控，無法描述實時系統(tǒng)的實時時序?qū)傩浴?br>　　在國內(nèi)外運行時驗證研究的基礎(chǔ)上，論文主要針對運行時驗證方法對實時時序?qū)傩缘尿炞C展開了深入的研究。首先，對運行時驗證的基本理論知識進行了深入研究，闡述了運行時驗證的特點，了解其在對列控系統(tǒng)安全驗證方面的應(yīng)用，并對運行時驗證的兩種基本方法進行了詳細的分析。
　　其次，對于列控系統(tǒng)這樣安全苛求的實時系統(tǒng)，現(xiàn)有的時序邏輯運行時驗證

3、算法不能對系統(tǒng)的實時性質(zhì)進行監(jiān)控驗證，表達能力不足。本文提出了能夠描述帶有顯式時間約束的度量時序邏輯(MTL)和時間命題時序邏輯(TPTL)的重寫語義。并在該語義的基礎(chǔ)上分別提出了基于MTL和基于TPTL的公式重寫型驗證監(jiān)控算法。這兩種監(jiān)控算法豐富了監(jiān)控需求的表達能力，描述出的時間約束性質(zhì)能夠?qū)崟r系統(tǒng)的時間軌跡進行監(jiān)控，從而克服了LTL無法對時間軌跡進行監(jiān)控的不足。
　　最后，為了更加方便的運用本文提出的運行時監(jiān)控算法對實時系統(tǒng)

4、實時屬性進行驗證，本文在底層Maude工具的基礎(chǔ)上對算法進行封裝，開發(fā)了可以進行自動化驗證的運行時驗證工具。為了對軌道交通車載控制器進行驗證，開發(fā)了可與實驗室半實物平臺進行數(shù)據(jù)傳輸?shù)慕涌?，用以接收列車運行過程中的實際數(shù)據(jù)。根據(jù)系統(tǒng)的高層規(guī)范提取列車運行需要滿足的監(jiān)控需求，并運用所開發(fā)的工具進行驗證和分析。另外，本文還以CTCS-3級列控系統(tǒng)的重要場景為案例進行了具體的運用演示。通過上述案例驗證了運行時監(jiān)控算法的可行性，演示了該工具在列控