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

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

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

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

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

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

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