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

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

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

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