基于時(shí)間自動(dòng)機(jī)的CBTC區(qū)域控制子系統(tǒng)形式化建模與驗(yàn)證.pdf

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

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

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