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

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

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

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

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