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

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

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

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

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

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