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

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

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

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

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