基于Timed RAISE的RBC切換建模與分析.pdf

1、CTCS(中國列車控制系統(tǒng))是我國鐵路當(dāng)中控制列車安全運(yùn)行，提高列車行車效率的重要裝備。RBC(無線閉塞中心)是CTCS-3級(jí)列控系統(tǒng)的重要組成部分，RBC切換是影響列車安全高效運(yùn)行的重要環(huán)節(jié)。列控系統(tǒng)是一種復(fù)雜的安全苛求系統(tǒng)，無論是在標(biāo)準(zhǔn)和規(guī)范的制定過程當(dāng)中，或是在系統(tǒng)的開發(fā)和設(shè)計(jì)階段，都不可避免的會(huì)存在著一些系統(tǒng)的漏洞或安全隱患。因此，使用形式化方法對(duì)RBC切換協(xié)議進(jìn)行建模與驗(yàn)證是十分必要的。
　　現(xiàn)階段所使用的形式化驗(yàn)證方法

2、較大部分都基于模型檢驗(yàn)，基于定理證明的形式化方法由于能夠描述具有無限狀態(tài)空間的系統(tǒng)，相比之下更適合應(yīng)用于結(jié)構(gòu)愈加復(fù)雜的列控系統(tǒng)，目前所使用的基于定理證明的形式化方法都只針對(duì)了列控系統(tǒng)中的某一種特性，很難全面的描述和驗(yàn)證系統(tǒng)。因此，本文采用Timed RAISE(工業(yè)軟件工程的嚴(yán)格方法)的形式化方法，對(duì)于CTCS-3級(jí)列控系統(tǒng)規(guī)范中的RBC切換協(xié)議進(jìn)行建模，對(duì)系統(tǒng)模型的正確性和實(shí)時(shí)性進(jìn)行驗(yàn)證。
　　首先，對(duì)Timed RAISE方法

3、進(jìn)行了介紹，通過一個(gè)具體的實(shí)例，描述了RSL(RAISE標(biāo)準(zhǔn)語言)語言的基本概念并說明了使用RSL語言進(jìn)行建模與驗(yàn)證的方法，分析說明了在模型驗(yàn)證當(dāng)中所使用的推理規(guī)則。
　　其次，對(duì) RBC切換流程進(jìn)行了分析，根據(jù)設(shè)備之間信息傳遞的過程，建立了交互信息圖。使用域的方法建立了RBC切換的域模型，在域模型中，將RBC切換整個(gè)連續(xù)的過程轉(zhuǎn)化為在時(shí)間上離散的過程，構(gòu)建了狀態(tài)轉(zhuǎn)移圖。結(jié)合交互信息圖中對(duì)于信息交互過程的描述，使用RSL語言對(duì)狀態(tài)