基于時間自動機的RBC控車場景建模與驗證.pdf

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

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

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