隨著我國(guó)鐵路事業(yè)的飛速發(fā)展,安全、高速成為鐵路系統(tǒng)的硬性標(biāo)準(zhǔn)。我國(guó)在引進(jìn)和借鑒歐洲ETCS列控系統(tǒng)的基礎(chǔ)上,研發(fā)了擁有自主產(chǎn)權(quán)的CTCS-3級(jí)中國(guó)列車控制系統(tǒng)。計(jì)算機(jī)聯(lián)鎖系統(tǒng)則是保證列車行車安全的基礎(chǔ)設(shè)備,主要是利用聯(lián)鎖軟件完成聯(lián)鎖功能的一種安全苛求性系統(tǒng),符合“故障-安全”原則。車站聯(lián)鎖控制直接關(guān)系到行車安全,也影響到車站作業(yè)的效率及行車組織工作,因此聯(lián)鎖系統(tǒng)在不斷更新和改進(jìn)。傳統(tǒng)的聯(lián)鎖軟件開發(fā)很多是用非形式化語(yǔ)言和自然語(yǔ)義來(lái)描述的,主要應(yīng)用于軟件工程的需求分析方法,在設(shè)計(jì)、分析和測(cè)試上已無(wú)法滿足計(jì)算機(jī)聯(lián)鎖系統(tǒng)的安全需求。所以使用形式化的方法對(duì)聯(lián)鎖系統(tǒng)進(jìn)行規(guī)范和說(shuō)明,不僅可以提高計(jì)算機(jī)聯(lián)鎖軟件的質(zhì)量,也有利于進(jìn)行更為嚴(yán)格的測(cè)試。計(jì)算機(jī)聯(lián)鎖主要是由微型計(jì)算機(jī)的軟件、硬件和一些電子、繼電器件組成的,具有高可靠性和安全性的實(shí)時(shí)控制系統(tǒng),聯(lián)鎖的意義就在于進(jìn)路控制過(guò)程的表述。通過(guò)結(jié)合6502繼電器的功能描述,對(duì)車站進(jìn)路聯(lián)鎖控制邏輯進(jìn)行完整說(shuō)明,使用具有嚴(yán)謹(jǐn)數(shù)學(xué)語(yǔ)義的形式化方法對(duì)聯(lián)鎖系統(tǒng)的安全規(guī)范進(jìn)行驗(yàn)證。本文在學(xué)習(xí)和研究鐵路聯(lián)鎖技術(shù)的基礎(chǔ)上,以車站進(jìn)路為場(chǎng)景,運(yùn)用形式化方法Event-B和多智... 

【文章來(lái)源】：蘭州交通大學(xué)甘肅省

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

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

【文章目錄】：
摘要
Abstract
引言
1 緒論
    1.1 研究背景
    1.2 研究目的和意義
    1.3 車站聯(lián)鎖國(guó)內(nèi)外研究綜述
    1.4 論文主要內(nèi)容及結(jié)構(gòu)框架
2 形式化描述與驗(yàn)證方法理論
    2.1 形式化方法
        2.1.1 形式化描述
        2.1.2 形式化方法驗(yàn)證和應(yīng)用
    2.2 Event-B方法及Rodin平臺(tái)
        2.2.1 Event-B基本結(jié)構(gòu)
        2.2.2 Event-B的數(shù)學(xué)體系
        2.2.3 Event-B模型精化和證明義務(wù)
        2.2.4 RODIN平臺(tái)
    2.3 MAS的方法理論
        2.3.1 Agent的概述
        2.3.2 多智能體系統(tǒng)(Multi-Agent System,MAS)
    2.4 本章小結(jié)
3 聯(lián)鎖的安全規(guī)范及邏輯語(yǔ)義描述
    3.1 鐵路聯(lián)鎖安全規(guī)范的提取方法
        3.1.1 進(jìn)路控制安全規(guī)范
        3.1.2 信號(hào)控制安全規(guī)范
        3.1.3 道岔控制安全規(guī)范
    3.2 聯(lián)鎖規(guī)范的邏輯語(yǔ)義描述
    3.3 本章小結(jié)
4 基于Event-B的聯(lián)鎖安全規(guī)范的描述和驗(yàn)證
    4.1 聯(lián)鎖系統(tǒng)安全規(guī)范Event-B描述方法
        4.1.1 聯(lián)鎖規(guī)范形式化描述及精化策略
        4.1.2 車站進(jìn)路聯(lián)鎖邏輯的Event-B初始模型
        4.1.3 車站進(jìn)路控制的Event-B建模分析
        4.1.4 車站進(jìn)路聯(lián)鎖控制的Event-B模型精化和驗(yàn)證
    4.2 車站進(jìn)路聯(lián)鎖Event-B驗(yàn)證方法
    4.3 本章小結(jié)
5 基于MAS和Event-B的分布式聯(lián)鎖安全的描述
    5.1 分布式實(shí)時(shí)系統(tǒng)
    5.2 MAS的體系結(jié)構(gòu)
    5.3 聯(lián)鎖安全描述
        5.3.1 Multi-Agent聯(lián)鎖層的安全規(guī)范描述
        5.3.2 Event-B的模型規(guī)范
        5.3.3 精化
    5.4 本章小結(jié)
結(jié)論
致謝
參考文獻(xiàn)
攻讀學(xué)位期間的研究成果


【參考文獻(xiàn)】：
期刊論文
[1]城軌綜合監(jiān)控系統(tǒng)的多Agent模型[J]. 董存祥.  鐵道工程學(xué)報(bào). 2013(12)
[2]基于Event-B的計(jì)算機(jī)聯(lián)鎖安全規(guī)范描述與驗(yàn)證[J]. 張?jiān)?王海峰.  鐵路計(jì)算機(jī)應(yīng)用. 2013(11)
[3]高速鐵路信號(hào)設(shè)備動(dòng)態(tài)管理方案研究[J]. 方明亮,胡恩華,魏盛昕,涂鵬飛.  鐵道通信信號(hào). 2013(03)
[4]CTCS-3級(jí)列控系統(tǒng)規(guī)范的建模與形式化驗(yàn)證方法研究[J]. 謝雨飛,唐濤,徐田華,趙林.  鐵道學(xué)報(bào). 2011(07)
[5]高速鐵路列控車載設(shè)備的發(fā)展[J]. 王馨.  鐵路通信信號(hào)工程技術(shù). 2010(05)
[6]形式化方法在列車運(yùn)行控制系統(tǒng)中的應(yīng)用[J]. 曹源,唐濤,徐田華,穆建成.  交通運(yùn)輸工程學(xué)報(bào). 2010(01)
[7]基于Repast平臺(tái)的多Agent仿真建模研究[J]. 蔣慧超,韋兆文.  計(jì)算機(jī)技術(shù)與發(fā)展. 2008(11)
[8]采用DFS策略的進(jìn)路搜索算法研究[J]. 胡媛,魏宗壽.  鐵路計(jì)算機(jī)應(yīng)用. 2007(09)
[9]計(jì)算機(jī)聯(lián)鎖軟件的Z規(guī)格說(shuō)明[J]. 王鐵江,酈萌.  鐵道學(xué)報(bào). 2003(04)
[10]我國(guó)鐵路信號(hào)系統(tǒng)的現(xiàn)狀與發(fā)展[J]. 姚麗娟.  鐵道通信信號(hào). 2003(04)

博士論文
[1]基于角色的多智能體社會(huì)模型研究與應(yīng)用[D]. 何漢明.西北工業(yè)大學(xué) 2006

碩士論文
[1]基于CSP的城軌CBTC聯(lián)鎖邏輯形式化建模與驗(yàn)證[D]. 馬慧.北京交通大學(xué) 2013
[2]基于Event-B的軟件需求形式化建模技術(shù)的研究[D]. 陳志慧.電子科技大學(xué) 2013
[3]高速鐵路列車運(yùn)行調(diào)整問(wèn)題研究[D]. 吳麗然.西南交通大學(xué) 2011
[4]CTCS-3級(jí)計(jì)算機(jī)聯(lián)鎖系統(tǒng)仿真實(shí)現(xiàn)[D]. 王亞?wèn)|.西南交通大學(xué) 2011
[5]B方法在配電自動(dòng)化系統(tǒng)中的應(yīng)用研究[D]. 孟蕓.河南大學(xué) 2010
[6]高速列車運(yùn)行控制系統(tǒng)仿真[D]. 廖麗軍.北京交通大學(xué) 2009
[7]基于人工智能的知識(shí)發(fā)現(xiàn)[D]. 臧其事.華東師范大學(xué) 2008
[8]基于B語(yǔ)言與TPN集成的形式化方法[D]. 姜夢(mèng)稚.華東師范大學(xué) 2006
[9]鐵路信號(hào)系統(tǒng)的Petri網(wǎng)建模與分析研究[D]. 鐘文燕.西南交通大學(xué) 2005



本文編號(hào)：3631470