基于SCADE的CBTC聯(lián)鎖建模與驗(yàn)證.pdf

1、城市軌道交通因其運(yùn)量大、占地少、高效節(jié)能、有利于保護(hù)環(huán)境等優(yōu)點(diǎn)，當(dāng)前已成為各大城市緩解交通擁堵壓力的首選方案?；谕ㄐ诺牧熊?chē)控制系統(tǒng)(Communication-based Train Control，CBTC)利用通信技術(shù)實(shí)現(xiàn)車(chē)-地之間雙向大容量的信息交互，具有安全、高效、靈活的特點(diǎn)，在城市軌道交通中得到了廣泛應(yīng)用。
　　計(jì)算機(jī)聯(lián)鎖(Computer-based Interlocking，CBI)系統(tǒng)是CBTC的關(guān)鍵系統(tǒng)，通過(guò)對(duì)

2、道岔、區(qū)段、信號(hào)等軌旁設(shè)備進(jìn)行監(jiān)控完成列車(chē)運(yùn)行預(yù)排、過(guò)程監(jiān)控等功能。CBI系統(tǒng)是一種安全苛求性系統(tǒng)，須要不斷的提高系統(tǒng)安全性來(lái)適應(yīng)城市軌道交通的發(fā)展。傳統(tǒng)的軟件設(shè)計(jì)及測(cè)試方法已經(jīng)無(wú)法滿(mǎn)足CBI系統(tǒng)繁雜地聯(lián)鎖控制邏輯及以故障安全為中心的安全需求?；谀Ｐ偷能浖_(kāi)發(fā)方法近年來(lái)在安全關(guān)鍵領(lǐng)域逐漸被接受。高安全性應(yīng)用開(kāi)發(fā)環(huán)境(Safety Critical Application Development Environment，SCADE)，以

3、基于模型的開(kāi)發(fā)方式為安全苛求系統(tǒng)提供完整的嵌入式開(kāi)發(fā)解決方法，其內(nèi)置的仿真器以及形式化驗(yàn)證器在軟件安全性和功能性上提供保證。本文基于SCADE對(duì)CBI系統(tǒng)聯(lián)鎖邏輯進(jìn)行建模、仿真及形式化驗(yàn)證，以此保障其安全性。本次論文主要工作有:
　　(1)介紹CBTC系統(tǒng)及其組成。
　　(2)分析CBTC系統(tǒng)聯(lián)鎖邏輯、基于CBTC的聯(lián)鎖特點(diǎn)功能以及CBTC系統(tǒng)中聯(lián)鎖與其他子系統(tǒng)的信息交互。
　　(3)以進(jìn)路建立過(guò)程為例，解析進(jìn)路建立過(guò)