基于時間自動機的CBTC區(qū)域控制子系統(tǒng)形式化建模與驗證.pdf

1、隨著城市化腳步的逐漸加快，CBTC(Communications-Based Train Control,基于通信的列車控制)系統(tǒng)已經(jīng)成為當(dāng)今世界城市軌道交通列控系統(tǒng)的發(fā)展趨勢。ZC(Zone Controller,區(qū)域控制器)作為CBTC系統(tǒng)的核心設(shè)備，是實現(xiàn)列車安全追蹤的關(guān)鍵，其可靠性直接關(guān)系到列車是否能安全運行。為了及時并準(zhǔn)確發(fā)現(xiàn)系統(tǒng)設(shè)計缺陷，在系統(tǒng)開發(fā)早期使用一種工具對系統(tǒng)進行描述和驗證就顯得尤為重要。形式化方法是以精確的數(shù)學(xué)語

2、言分析和驗證系統(tǒng)的技術(shù)和工具。本文采用形式化方法對ZC進行建模和驗證，目的在于保證ZC設(shè)計的正確性和安全性。
　　首先，論文分析了當(dāng)前主流的形式化方法，根據(jù)安全苛求系統(tǒng)的設(shè)計要求，提出了形式化方法時間自動機理論及其自動驗證工具UPPAAL。
　　其次，在對CBTC的基本結(jié)構(gòu)和運行原理進行分析的基礎(chǔ)上，對本文的重點ZC的工作原理進行深入的分析，提出了系統(tǒng)的功能和性能需求。由于ZC是一個復(fù)雜實時系統(tǒng)，可將其按照功能劃分為四大模塊

3、：列車管理、移動授權(quán)、ZC切換以及ZC與CBTC其他子系統(tǒng)信息交互。然后分別對它們的流程進行了設(shè)計。根據(jù)列車在CBTC區(qū)域運行的流程設(shè)計，利用時間自動機分別對ZC的功能進行建模，通過設(shè)置通道和共享變量實現(xiàn)幾個時間自動機的通信，將其組成為一個完整的時間自動機網(wǎng)絡(luò)模型。
　　最后，利用 UPPAAL對所建模型進行模擬得到消息序列圖，分析了列車在 CBTC區(qū)域運行過程中狀態(tài)的變化以及各子系統(tǒng)間的通信。然后應(yīng)用 BNF語句提煉出系統(tǒng)的功能