基于時(shí)間自動(dòng)機(jī)的RBC控車場(chǎng)景建模與驗(yàn)證.pdf

1、CTCS-3級(jí)列控系統(tǒng)是鐵路信號(hào)領(lǐng)域的主要技術(shù)設(shè)備，它擔(dān)負(fù)著指揮列車運(yùn)行，保證行車安全和提高運(yùn)輸效率的重要任務(wù)。無(wú)線閉塞中心(Raid Block Center，RBC)系統(tǒng)是CTCS-3級(jí)列控系統(tǒng)地面設(shè)備中的核心設(shè)備，它是實(shí)現(xiàn)安全、高效控車的關(guān)鍵。由于RBC系統(tǒng)作為安全苛求系統(tǒng)(safety critical system)，不僅功能復(fù)雜，而且實(shí)時(shí)性要求極高，因此對(duì)RBC系統(tǒng)設(shè)計(jì)的正確性和可靠性提出了更高的要求。然而傳統(tǒng)的系統(tǒng)設(shè)計(jì)方法

2、存在不能及時(shí)發(fā)現(xiàn)軟件錯(cuò)誤和隱患的缺陷，本文探索采用基于時(shí)間自動(dòng)機(jī)理論的形式化方法對(duì)RBC系統(tǒng)的軟件進(jìn)行安全性設(shè)計(jì)和驗(yàn)證，以期提高RBC系統(tǒng)設(shè)計(jì)開(kāi)發(fā)的安全、可靠和正確性。
　　對(duì)RBC系統(tǒng)的形式化建模與驗(yàn)證的實(shí)質(zhì)就是尋求一個(gè)同被研究原型有極密切映象關(guān)系的時(shí)間自動(dòng)機(jī)模型研究系統(tǒng)。本文在分析既有RBC形式化建模技術(shù)及其優(yōu)缺點(diǎn)的基礎(chǔ)上，研究和探索了根據(jù)系統(tǒng)規(guī)范對(duì)RBC系統(tǒng)基于時(shí)間自動(dòng)機(jī)理論進(jìn)行形式化建模和驗(yàn)證。由于RBC系統(tǒng)是一個(gè)大型的、

3、功能復(fù)雜的實(shí)時(shí)系統(tǒng)，為了更加直觀清晰地描述系統(tǒng)，以CTCS-3級(jí)列控系統(tǒng)標(biāo)準(zhǔn)規(guī)范為依據(jù)，以RBC系統(tǒng)的主要控車運(yùn)營(yíng)場(chǎng)景作為切入點(diǎn)，分析各個(gè)場(chǎng)景中RBC系統(tǒng)的控車流程，建立了主要功能場(chǎng)景的時(shí)間自動(dòng)機(jī)模型，并通過(guò)通道和全局變量組建成時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)模型。然后在UPPAAL工具中對(duì)所建模型進(jìn)行模擬仿真，提取系統(tǒng)的關(guān)鍵功能點(diǎn)，并將其轉(zhuǎn)化為BNF語(yǔ)法中的語(yǔ)句，在UPPAAL驗(yàn)證器中對(duì)網(wǎng)絡(luò)模型的正確性進(jìn)行驗(yàn)證。利用UPPAAL驗(yàn)證的結(jié)果表明，所建基于