隨著我國(guó)經(jīng)濟(jì)的迅速發(fā)展,城市的人口大量增加,城市交通運(yùn)輸壓力不斷增大。城市軌道交通以其速度快、運(yùn)輸力強(qiáng)、舒適性高以及對(duì)環(huán)境造成的污染低等優(yōu)點(diǎn)成為大中型城市解決擁堵問題的首選,CBTC （Communication Based Train Control）技術(shù)在此背景下應(yīng)運(yùn)而生,并以其顯著優(yōu)勢(shì)逐漸成為城市軌道交通信號(hào)系統(tǒng)的首選方案。聯(lián)鎖系統(tǒng)作為CBTC系統(tǒng)的重要組成部分,是行車安全的重要保障設(shè)備。聯(lián)鎖系統(tǒng)的安全要求級(jí)別較高,因此采用高安全性軟件開發(fā)聯(lián)鎖系統(tǒng)是十分必要的。高安全性應(yīng)用開發(fā)環(huán)境SCADE （Safety-Critical Application Development Environment）為軟件開發(fā)人員提供了完整的基于模型的開發(fā)解決方案,以此來降低開發(fā)成本、減少開發(fā)風(fēng)險(xiǎn)和縮短驗(yàn)證時(shí)間。本文以鄭州地鐵一號(hào)線的一個(gè)聯(lián)鎖區(qū)為分析對(duì)象,利用SCADE對(duì)聯(lián)鎖的主要功能進(jìn)行建模并驗(yàn)證。首先對(duì)國(guó)內(nèi)外的聯(lián)鎖系統(tǒng)研究情況以及聯(lián)鎖邏輯建模的情況進(jìn)行了探討,對(duì)CBTC的主要結(jié)構(gòu)和子系統(tǒng)進(jìn)行了闡述。研究了SCADE的基礎(chǔ)理論,探討了基于同步編程理論的兩種建模方法：數(shù)據(jù)流圖方法和安全狀態(tài)機(jī)方法,分... 

【文章來源】：西南交通大學(xué)四川省 211工程院校 教育部直屬院校

【文章頁(yè)數(shù)】：76 頁(yè)

【學(xué)位級(jí)別】：碩士

【文章目錄】：
摘要
abstract
第1章 緒論
    1.1 研究背景和意義
    1.2 聯(lián)鎖的研究狀況
    1.3 CBTC及聯(lián)鎖簡(jiǎn)介
        1.3.1 CBTC系統(tǒng)概述
        1.3.2 城軌聯(lián)鎖子系統(tǒng)概述
    1.4 論文的主要內(nèi)容
第2章 SCADE及其功能研究
    2.1 SCADE的理論基礎(chǔ)
    2.2 SCADE的軟件開發(fā)方法
    2.3 數(shù)據(jù)流圖建模方法
    2.4 SCADE的其他功能
        2.4.1 模型仿真與驗(yàn)證
        2.4.2 代碼自動(dòng)生成
    2.5 本章小結(jié)
第3章 基于SCADE的聯(lián)鎖邏輯建模
    3.1 聯(lián)鎖
    3.2 道岔模塊
        3.2.1 道岔轉(zhuǎn)換模塊
        3.2.2 道岔封鎖模塊
        3.2.3 道岔整體模塊圖
    3.3 進(jìn)路模塊
        3.3.1 進(jìn)路請(qǐng)求模塊
        3.3.2 進(jìn)路檢查模塊
        3.3.3 接近模塊
        3.3.4 區(qū)段方向鎖模塊
        3.3.5 選排一致檢查模塊
        3.3.6 進(jìn)路整體模塊圖
    3.4 信號(hào)開放模塊
        3.4.1 直向進(jìn)路信號(hào)模塊
        3.4.2 側(cè)向進(jìn)路信號(hào)模塊
        3.4.3 引導(dǎo)信號(hào)模塊
        3.4.4 自動(dòng)進(jìn)路模塊
        3.4.5 快速通過模塊
    3.5 解鎖模塊
    3.6 模塊集成
    3.7 本章小結(jié)
第4章 仿真與C代碼的自動(dòng)生成
    4.1 聯(lián)鎖模型的仿真
        4.1.1 進(jìn)路模塊的仿真
        4.1.2 道岔模塊的仿真
        4.1.3 信號(hào)模塊的仿真
    4.2 模型的形式化驗(yàn)證
        4.2.1 形式化驗(yàn)證方法
        4.2.2 模型的形式化驗(yàn)證
    4.3 C代碼生成
        4.3.1 代碼生成的配置
        4.3.2 模型的C代碼生成
    4.4 本章小結(jié)
結(jié)論
致謝
參考文獻(xiàn)
附錄1 模塊形式化驗(yàn)證
附錄2 生成的主要C代碼
攻讀碩士學(xué)位期間發(fā)表的論文及科研成果


【參考文獻(xiàn)】：
期刊論文
[1]城市軌道交通信號(hào)控制系統(tǒng)中4種接近區(qū)段的定義和計(jì)算[J]. 黃克勇.  城市軌道交通研究. 2015(05)
[2]淺談CBTC系統(tǒng)中區(qū)域控制器和外部聯(lián)鎖功能接口[J]. 馬睿.  信息通信. 2013(04)
[3]CBTC系統(tǒng)中聯(lián)鎖與ATP接口簡(jiǎn)析[J]. 施小敏.  鐵路通信信號(hào)工程技術(shù). 2013(02)
[4]計(jì)算機(jī)聯(lián)鎖在CBTC系統(tǒng)中的兩種集成方式[J]. 趙曉峰.  鐵道通信信號(hào). 2012(11)
[5]簡(jiǎn)析CBTC系統(tǒng)中聯(lián)鎖與區(qū)域控制器的關(guān)系[J]. 張昌平.  鐵路通信信號(hào)工程技術(shù). 2012(03)
[6]基于SCADE的形式化驗(yàn)證技術(shù)研究[J]. 林楓.  測(cè)控技術(shù). 2011(12)
[7]CBTC系統(tǒng)中的聯(lián)鎖技術(shù)研究[J]. 凌祝軍.  鐵道通信信號(hào). 2009(09)
[8]SCADE軟件開發(fā)方法研究[J]. 胡鋼偉,李振水,高亞奎.  系統(tǒng)仿真學(xué)報(bào). 2008(S2)
[9]計(jì)算機(jī)聯(lián)鎖控制系統(tǒng)故障模式影響分析[J]. 劉伯鴻.  鐵道技術(shù)監(jiān)督. 2007(02)
[10]基于時(shí)間自動(dòng)機(jī)的道岔自動(dòng)控制研究[J]. 周清雷,姬莉霞.  控制工程. 2004(S2)

博士論文
[1]城市軌道交通CBTC系統(tǒng)關(guān)鍵技術(shù)研究[D]. 劉曉娟.蘭州交通大學(xué) 2009

碩士論文
[1]基于SCADE的CBTC區(qū)域控制器建模與驗(yàn)證[D]. 李容.西南交通大學(xué) 2015
[2]基于SCADE的CBTC聯(lián)鎖建模與驗(yàn)證[D]. 陳淑珍.西南交通大學(xué) 2015
[3]城市軌道交通聯(lián)鎖系統(tǒng)可靠性及安全性分析研究[D]. 張重.蘭州交通大學(xué) 2014
[4]城市軌道交通移動(dòng)授權(quán)設(shè)計(jì)與實(shí)現(xiàn)[D]. 吳曦.西南交通大學(xué) 2014
[5]基于SCADE的信息物理融合系統(tǒng)的分析和設(shè)計(jì)方法[D]. 彭濤.廣東工業(yè)大學(xué) 2014
[6]ATS系統(tǒng)環(huán)境模擬與測(cè)試平臺(tái)的設(shè)計(jì)和實(shí)現(xiàn)[D]. 周正.西南交通大學(xué) 2014
[7]基于SCADE的定位系統(tǒng)設(shè)計(jì)及驗(yàn)證[D]. 李俊杰.西南交通大學(xué) 2014
[8]基于CBTC系統(tǒng)的聯(lián)鎖邏輯研究[D]. 楊淘.西南交通大學(xué) 2014
[9]城市軌道交通區(qū)域計(jì)算機(jī)聯(lián)鎖仿真系統(tǒng)的研究[D]. 陳璐.蘭州交通大學(xué) 2013
[10]基于CSP的城軌CBTC聯(lián)鎖邏輯形式化建模與驗(yàn)證[D]. 馬慧.北京交通大學(xué) 2013



本文編號(hào)：3355722