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

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

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

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