基于安全狀態(tài)機(jī)的計(jì)算機(jī)聯(lián)鎖系統(tǒng)建模與分析.pdf

1、城市軌道交通以其安全可靠、污染低、運(yùn)量大、速度快、受其他交通方式干擾小等特點(diǎn)，成為解決城市交通擁堵問題的首選方案?；谕ㄐ诺牧熊嚳刂葡到y(tǒng)(Communication-based Train Control，CBTC)具有軌旁設(shè)備少、列車追蹤間隔短、運(yùn)營效率高等優(yōu)點(diǎn)，是列控技術(shù)的重要發(fā)展方向。計(jì)算機(jī)聯(lián)鎖(ComputerBased Interlocking，CBI)系統(tǒng)作為CBTC的核心子系統(tǒng)之一，是一個(gè)安全苛求系統(tǒng)，對(duì)列車的安全運(yùn)行有著

2、重要的影響，具有極高的安全性和可靠性要求，因此，如何保證計(jì)算機(jī)聯(lián)鎖系統(tǒng)設(shè)計(jì)開發(fā)的安全性和正確性具有十分重要的意義。
　　安全狀態(tài)機(jī)(Safe State Machine，SSM)是一種圖形化的同步建模語言，具有并發(fā)性、層次性、良好的優(yōu)先級(jí)搶占機(jī)制和通信機(jī)制，模型清晰、簡潔，具有良好的可讀性，能夠描述安全苛求系統(tǒng)復(fù)雜的邏輯過程。SSM形式化的理論基礎(chǔ)避免了傳統(tǒng)需求分析方法中的模糊性和二義性等缺陷;同時(shí)，高安全性應(yīng)用開發(fā)環(huán)境(Safe

3、ty Critical Application Development Environment，SCADE)支持SSM的建模、仿真和形式化驗(yàn)證，為SSM在實(shí)際工程中的應(yīng)用提供了基礎(chǔ)。
　　本文選擇SSM來對(duì)CBI系統(tǒng)進(jìn)行建模和分析，主要包括以下幾個(gè)方面:
　　(1)分析了SSM的理論基礎(chǔ)、建模特征及格局轉(zhuǎn)移機(jī)制，并介紹了SSM在SCADE中的建模、仿真及形式化分析方法;
　　(2)分析了CBI的基本結(jié)構(gòu)及CBTC系統(tǒng)中

4、的CBI的聯(lián)鎖功能，分析了CBI與CBTC子系統(tǒng)的交互關(guān)系，對(duì)比了CBTC下CBI與傳統(tǒng)的聯(lián)鎖系統(tǒng)的區(qū)別。
　　(3)將CBI劃分為道岔、進(jìn)路、信號(hào)機(jī)三個(gè)功能模塊，分析了各個(gè)模塊具體的邏輯條件;然后基于SSM的理論，利用SCADE對(duì)各個(gè)模塊進(jìn)行了建模，具體包括道岔請(qǐng)求、選排、鎖閉邏輯，進(jìn)路請(qǐng)求、檢查邏輯，區(qū)段方向邏輯及信號(hào)開放邏輯等;最后利用SCADE的數(shù)據(jù)流圖將道岔、進(jìn)路及信號(hào)機(jī)三個(gè)模塊集成為CBI邏輯模型。
　　(4)通