列車運(yùn)行控制系統(tǒng)分層形式化建模與驗(yàn)證分析.pdf

1、列車運(yùn)行控制系統(tǒng)(簡稱“列控系統(tǒng)”)是將先進(jìn)的控制技術(shù)、通信技術(shù)、計(jì)算機(jī)技術(shù)與鐵路信號技術(shù)融為一體,保證軌道交通安全、正點(diǎn)、高密度運(yùn)行的自動化系統(tǒng)。隨著計(jì)算機(jī)在列控系統(tǒng)中的廣泛應(yīng)用,硬件和軟件規(guī)模不斷擴(kuò)大,系統(tǒng)的復(fù)雜性有了很大的提高,呈現(xiàn)出復(fù)雜的系統(tǒng)特性(并發(fā)性、實(shí)時性和混合屬性等等)。作為一個復(fù)雜安全苛求系統(tǒng),列控系統(tǒng)中任何故障都有可能造成重大的人身傷亡和財(cái)產(chǎn)損失,如何保證系統(tǒng)的正確性,尋找一套全面的、有效的建模與驗(yàn)證方法是非常必要的

2、。相比仿真和測試技術(shù),基于嚴(yán)格數(shù)學(xué)定義的形式化方法不僅能精確、清晰地描述系統(tǒng)結(jié)構(gòu)和相關(guān)特性,而且能對特性進(jìn)行驗(yàn)證,近年來已經(jīng)成為列控系統(tǒng)建模和驗(yàn)證的一種重要理論方法。
　　 論文引入系統(tǒng)層次化建模概念,利用面向?qū)ο蟮慕Ｋ枷牒突趫鼍暗南到y(tǒng)設(shè)計(jì)理念,提出了一套包含系統(tǒng)層、場景層、組件層和功能層的列控系統(tǒng)層次化模型。在此基礎(chǔ)上,提出了一個集成HCSP(Hybrid Communication Sequential Process)

3、、CHARON和TL(Temporal Logic)的列控系統(tǒng)分層形式化建模與驗(yàn)證框架。該框架不僅適合列控系統(tǒng)各種特性的驗(yàn)證分析,而且建立的模型具有可繼承性、重用性,在保證系統(tǒng)模型一致性的基礎(chǔ)上,提高了建模的效率。
　　 論文深入分析了列控系統(tǒng)運(yùn)營場景實(shí)時性的驗(yàn)證問題,提出了六種適合于列控系統(tǒng)運(yùn)營場景描述的時間約束類型:周期性、延遲、時間等待、超時、截止期限和時間中斷；提出了HCSP的子集模型到時間自動機(jī)網(wǎng)絡(luò)模型的轉(zhuǎn)換規(guī)則；給出

4、了運(yùn)營場景實(shí)時性約束的TCTL(Timed Computation Tree Logic)描述；實(shí)現(xiàn)了運(yùn)營場景中相關(guān)實(shí)時屬性的驗(yàn)證流程。
　　 論文深入研究了列控系統(tǒng)運(yùn)營場景的混合屬性驗(yàn)證問題,指出了傳統(tǒng)的混雜系統(tǒng)建模與驗(yàn)證方法在刻畫列控系統(tǒng)場景中通信行為上存在的不足。并根據(jù)現(xiàn)有HCSP方法的不足,提出了HCSP的假設(shè)條件；結(jié)合混合自動機(jī)的語義,提出了HCSP模型到混合自動機(jī)模型的轉(zhuǎn)換規(guī)則；給出了運(yùn)營場景中混合屬性的ACTL(A

5、ction Computation Tree Logic)表達(dá)；實(shí)現(xiàn)了運(yùn)營場景中相關(guān)混合屬性的驗(yàn)證流程。
　　 論文最后選取了CTCS-3級列控系統(tǒng)總體技術(shù)方案中兩個典型的運(yùn)營場景(RBC(Radio Block Center)切換場景和行車許可場景)作為案例來分析。通過對RBC切換場景和行車許可場景的分層形式化建模與驗(yàn)證分析,驗(yàn)證了列控系統(tǒng)的實(shí)時性和混合屬性,最大限度的避免了系統(tǒng)設(shè)計(jì)上的缺陷和錯誤,為進(jìn)一步解決列控系統(tǒng)建模與驗(yàn)