基于時(shí)間自動(dòng)機(jī)的CTCS-3級(jí)列控車(chē)載設(shè)備建模與驗(yàn)證.pdf

1、鐵路系統(tǒng)歷來(lái)對(duì)安全性要求較高,CTCS-3級(jí)列控設(shè)備作為高速列車(chē)的控制系統(tǒng)對(duì)安全性的要求更高。車(chē)載設(shè)備系統(tǒng)是中國(guó)鐵路CTCS-3級(jí)列控系統(tǒng)中的重要組成部分,UPPAAL是一種基于時(shí)間自動(dòng)機(jī)理論的實(shí)時(shí)系統(tǒng)分析建模驗(yàn)證工具,使用UPPAAL對(duì)CTCS-3級(jí)列控系統(tǒng)車(chē)載設(shè)備中的車(chē)載安全計(jì)算機(jī)VC、司機(jī)-車(chē)載設(shè)備接口DMI和無(wú)線(xiàn)閉塞中心RBC進(jìn)行分析建模驗(yàn)證,可以驗(yàn)證車(chē)載設(shè)備系統(tǒng)的特性。研究車(chē)載設(shè)備系統(tǒng)的建模,對(duì)于完善車(chē)載設(shè)備仿真系統(tǒng)性能、加快

2、車(chē)載設(shè)備系統(tǒng)軟件設(shè)計(jì)、節(jié)省現(xiàn)場(chǎng)測(cè)試成本等具有重要的現(xiàn)實(shí)意義。
　　 論文完成的主要工作如下:
　　 1.概述了國(guó)內(nèi)外基于形式化方法和時(shí)間自動(dòng)機(jī)理論的列控系統(tǒng)建模的研究現(xiàn)狀,提出了用時(shí)間自動(dòng)機(jī)對(duì)車(chē)載設(shè)備建模的意義。
　　 2.介紹了CTCS-3級(jí)列控車(chē)載設(shè)備結(jié)構(gòu)、功能以及工作模式。
　　 3.分析了工作在CTCS-3級(jí)時(shí)的車(chē)載任務(wù)啟動(dòng)流程、車(chē)載越行流程、列車(chē)冒進(jìn)后防護(hù)流程、司機(jī)觸發(fā)的SH流程和車(chē)載任務(wù)結(jié)束流

3、程,建立了各個(gè)工作流程的狀態(tài)轉(zhuǎn)換圖,說(shuō)明了車(chē)載設(shè)備的信息交互及狀態(tài)轉(zhuǎn)換過(guò)程。
　　 4.介紹了時(shí)間自動(dòng)機(jī)理論及其模型檢驗(yàn)工具UPPAAL的使用方法。
　　 5.基于時(shí)間自動(dòng)機(jī)理論對(duì)VC、DMI和RBC分別建模:根據(jù)研究對(duì)象的特點(diǎn),在合理的抽象和假設(shè)之后,確定了各個(gè)模型的狀態(tài),狀態(tài)轉(zhuǎn)換路徑、狀態(tài)轉(zhuǎn)換的約束條件和觸發(fā)事件,得到了車(chē)載設(shè)備的各個(gè)時(shí)間自動(dòng)機(jī)模型。
　　 6.通過(guò)使用UPPAAL對(duì)車(chē)載設(shè)備系統(tǒng)的時(shí)間自動(dòng)機(jī)模