基于CBTC的聯(lián)鎖系統(tǒng)進(jìn)路控制形式化建模與驗(yàn)證.pdf

1、城市軌道交通在通信、控制、計(jì)算機(jī)技術(shù)大發(fā)展的背景下已經(jīng)成為許多國(guó)家和城市建設(shè)的重點(diǎn)。計(jì)算機(jī)聯(lián)鎖系統(tǒng)是城市軌道交通系統(tǒng)的重要組成部分，對(duì)防護(hù)列車運(yùn)行安全具有重要意義。隨著計(jì)算機(jī)技術(shù)在CBTC(Communication Based Train Control)聯(lián)鎖系統(tǒng)的廣泛應(yīng)用，系統(tǒng)的復(fù)雜性和不確定性大大增加，對(duì)系統(tǒng)的安全保障也隨之變得更加困難，因此聯(lián)鎖系統(tǒng)在設(shè)計(jì)開發(fā)階段需要有科學(xué)完備的分析和驗(yàn)證。由于傳統(tǒng)的需求分析方法具有不完備的缺點(diǎn)，

2、本文采用時(shí)間自動(dòng)機(jī)的形式化方法對(duì)CBTC聯(lián)鎖系統(tǒng)進(jìn)行建模分析，以此提高系統(tǒng)的安全性。
　　本文首先對(duì)CBTC聯(lián)鎖系統(tǒng)進(jìn)行了詳細(xì)的介紹，分析了聯(lián)鎖系統(tǒng)的主要功能需求，并對(duì)聯(lián)鎖在進(jìn)路控制流程中的功能模塊進(jìn)行了劃分，分析了CBTC聯(lián)鎖系統(tǒng)進(jìn)路控制的主要流程。
　　然后，根據(jù)聯(lián)鎖邏輯過程以及時(shí)序流程，提取聯(lián)鎖系統(tǒng)的功能約束，依據(jù)時(shí)間自動(dòng)機(jī)理論對(duì)CBTC聯(lián)鎖系統(tǒng)進(jìn)路控制流程中的道岔模塊、進(jìn)路模塊、信號(hào)機(jī)模塊進(jìn)行了形式化建模，主要包括道

3、岔請(qǐng)求、道岔選排、道岔鎖閉、信號(hào)請(qǐng)求、進(jìn)路檢查、區(qū)段鎖閉、信號(hào)開放等功能模型，最后得到了CBTC聯(lián)鎖系統(tǒng)進(jìn)路控制過程的時(shí)間自動(dòng)機(jī)模型，并利用時(shí)間自動(dòng)機(jī)的時(shí)鐘約束特性設(shè)計(jì)了聯(lián)鎖系統(tǒng)的“緩放”、“緩吸”邏輯，最后利用共享全局變量和通道的方式組建了CBTC聯(lián)鎖邏輯的時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)。
　　最后，借助時(shí)間自動(dòng)機(jī)工具UPPAAL對(duì)時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)進(jìn)行仿真得到進(jìn)路控制流程的時(shí)序圖，分析了系統(tǒng)模塊之間的通信過程以及狀態(tài)遷移;并人工提取所建進(jìn)路控制系