基于時間自動機的列控中心軟件形式化建模與驗證.pdf

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

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

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