高速鐵路列車運行控制系統(tǒng)的形式建模與驗證方法研究.pdf

1、高速鐵路列車運行控制系統(tǒng)(簡稱:列控系統(tǒng))融入了先進的計算機、通信以及控制技術,極大地提升了系統(tǒng)的效率和安全性。由于系統(tǒng)的硬件集成度不斷提高,大量軟件參與系統(tǒng)控制,使得系統(tǒng)特性也呈現(xiàn)出結構分布、實時性強、響應快速等多樣化的趨勢,系統(tǒng)特性的驗證也愈加困難,因此需要找到一條更為有效、全面的方法實現(xiàn)列控系統(tǒng)的特性驗證,進一步提升系統(tǒng)的性能或完善系統(tǒng)功能?；趪栏駭?shù)學定義的形式化方法,由于其能夠精確、清晰地描述系統(tǒng)結構和相關特性,同時能夠驗證系

2、統(tǒng)的相關特性,近年來在列控系統(tǒng)領域得到迅速發(fā)展,并且已經(jīng)成為描述和驗證高速鐵路列控系統(tǒng)特性的一種重要方法。
　　 論文對列控系統(tǒng)的形式化建模、描述以及驗證方法的應用展開了綜述。分析了RAISE(Rigorous Approach to Industrial Software Engineering,工業(yè)軟件工程的嚴格方法)形式化方法在列控系統(tǒng)中建模與驗證的優(yōu)勢,并在此基礎上,首次將Timed RAISE(時間化RAISE)引入列

3、控系統(tǒng)驗證領域。
　　 論文研究了基于域+Timed RAISE的高速鐵路列控系統(tǒng)的建模和描述方法。結合高速鐵路列控系統(tǒng)的實際特點以及復雜性,提出了一種域方法作為系統(tǒng)描述的切入。域方法的主要思想是將系統(tǒng)劃分為規(guī)模較小的域模型,根據(jù)域的驗證結果以及域之間的分解與組合關系,能夠最終實現(xiàn)大系統(tǒng)的特性驗證。
　　 論文詳細給出了域的元組、域的組合分解以及域特性的組合分解等相關定義和定理,這些定義與定理也是域方法理論體系的關鍵組成

4、部分。為實現(xiàn)對域方法的更好說明,對典型的高速鐵路列控系統(tǒng)-CTCS-3(China Train Control Systemlevel3)級列控系統(tǒng)進行了實際的域的劃分、域模型的建立、域特性的分析、域特性的組合分解以及子域的劃分,實現(xiàn)了對域方法理論體系的有力支撐。
　　 論文研究了基于域+Timed RAISE的高速鐵路列控系統(tǒng)的驗證方法。對高速鐵路列控系統(tǒng)常見的運營場景描述相關特性、系統(tǒng)功能以及系統(tǒng)性能等三類重要的域特性進行了

5、詳細分析,并給出了三類域特性中的場景交互一致性、安全功能以及實時性的定義和數(shù)學描述,并作為系統(tǒng)特性驗證的重要依據(jù)。
　　 論文實現(xiàn)了域模型與Timed RAISE結合,給出了域模型轉換為TRSL(TimedRAISE Specification Language)的具體規(guī)則,同時也給出了在系統(tǒng)TRSL描述的證明過程中相應的推理規(guī)則和證明方法。
　　 論文對基于域+Timed RAISE的描述和驗證方法的具體應用進行了分析

6、和舉例。通過對RBC(Radio Block Center,無線閉塞中心)切換場景的交互一致性驗證、等級轉換(CTCS-2級至CTCS-3級)場景的實時性驗證以及兩車區(qū)間追蹤案例中的安全功能進行了實際的域(子域)的劃分、系統(tǒng)模型建立、Timed RAISE具體描述以及驗證過程。僅為說明基于域+Timed RAISE方法的正確性,將各驗證案例都進行了相應的簡化和假設。最終給出了結果:列車通過RBC邊界的條件下,車載設備與兩個RBC的共同交