基于時(shí)間自動(dòng)機(jī)的列控中心軟件形式化建模與驗(yàn)證.pdf

1、列車運(yùn)行控制系統(tǒng)是我國(guó)高速鐵路的核心技術(shù)之一，目前我國(guó)高速鐵路均采用CTCS-3級(jí)列控系統(tǒng)作為統(tǒng)一技術(shù)平臺(tái)。CTCS-3級(jí)列控系統(tǒng)是一個(gè)安全性要求極高的系統(tǒng)，對(duì)其進(jìn)行功能及性能的安全性驗(yàn)證和評(píng)估非常重要。采用計(jì)算機(jī)技術(shù)，在實(shí)驗(yàn)室搭建CTCS-3級(jí)列控系統(tǒng)仿真平臺(tái)對(duì)其進(jìn)行輔助研究和預(yù)研驗(yàn)證具有實(shí)際意義。列控中心(TCC)是CTCS的關(guān)鍵設(shè)備之一。在CTCS-2級(jí)列控系統(tǒng)的地面設(shè)備中，TCC作為核心安全設(shè)備，產(chǎn)生控車信息控制列車運(yùn)行，是保證

2、列車安全運(yùn)行的關(guān)鍵信號(hào)設(shè)備。作為CTCS-3后備系統(tǒng)，TCC是不可缺少的重要組成設(shè)備，其可靠性和實(shí)時(shí)性影響到整個(gè)高速鐵路的安全高效運(yùn)行，保證TCC軟件的可靠性和實(shí)時(shí)性顯得尤為重要。
　　本文結(jié)合時(shí)間自動(dòng)機(jī)理論，對(duì)TCC軟件進(jìn)行形式化語(yǔ)義描述，使用基于時(shí)間自動(dòng)機(jī)理論的建模驗(yàn)證工具對(duì)TCC軟件進(jìn)行建模，并驗(yàn)證分析軟件特性，從而保證在軟件設(shè)計(jì)邏輯下，TCC可以高效準(zhǔn)確地生成控車信息。提出兩種適合于TCC軟件的建模方法，分別是基于時(shí)間自動(dòng)

3、機(jī)的分層建模方法和采用UML與時(shí)間自動(dòng)機(jī)相結(jié)合的建模方法。針對(duì)分層建模方法，以有源應(yīng)答器報(bào)文編制流程為例:首先根據(jù)流程的特點(diǎn)，對(duì)有源應(yīng)答器報(bào)文編制功能進(jìn)行分層設(shè)計(jì);其次，經(jīng)過(guò)合理的抽象和假設(shè)，對(duì)分層設(shè)計(jì)建立成員時(shí)間自動(dòng)機(jī);再次，通過(guò)設(shè)置通道和全局變量，在模型驗(yàn)證工具中建立時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò);最后，在工具中模擬驗(yàn)證模型的功能和性能。針對(duì)UML與時(shí)間自動(dòng)機(jī)相結(jié)合的建模方法，以TCC的軌道電路編碼功能為例:首先進(jìn)行軟件設(shè)計(jì)的分類整理，根據(jù)軟件概要