本文選題：聯(lián)鎖系統(tǒng) + 形式化方法　； 參考：《中國(guó)鐵道科學(xué)研究院》2017年博士論文

【摘要】：作為基于通信的列車控制(Communication Based Train Control,CBTC)系統(tǒng)的安全關(guān)鍵設(shè)備,聯(lián)鎖系統(tǒng)的結(jié)構(gòu)、功能邏輯復(fù)雜,軟硬件集成度較高,是典型的復(fù)雜安全苛求系統(tǒng)。如何保證聯(lián)鎖系統(tǒng)開(kāi)發(fā)的正確性和安全性,尋求一套全面、有效的建模與驗(yàn)證方法已經(jīng)成為CBTC系統(tǒng)中亟需解決的問(wèn)題。近年來(lái),基于嚴(yán)格數(shù)學(xué)定義的形式化方法越來(lái)越顯示出它的優(yōu)越性,不僅能夠準(zhǔn)確、清晰地描述系統(tǒng)的結(jié)構(gòu)與功能,而且能夠?qū)ο到y(tǒng)特性進(jìn)行驗(yàn)證,已經(jīng)成為CBTC聯(lián)鎖系統(tǒng)建模與驗(yàn)證的一種重要理論方法�；诖�,針對(duì)CBTC聯(lián)鎖系統(tǒng)形式化建模與驗(yàn)證的關(guān)鍵問(wèn)題,本文從模型可重用性、并發(fā)性、模型轉(zhuǎn)換方法,以及組合形式化方法四個(gè)方面展開(kāi)了深入研究。本論文的主要成果和創(chuàng)新點(diǎn)如下:(1)針對(duì)CBTC聯(lián)鎖系統(tǒng)模型狀態(tài)空間復(fù)雜、重復(fù)構(gòu)件模型成本巨大的問(wèn)題,本文提出并實(shí)現(xiàn)了一種基于分層有色Petri網(wǎng)(HCPN)的CBTC聯(lián)鎖系統(tǒng)模型模板。該模板屬于分層的參數(shù)化模型,可重用性較強(qiáng),適用于不同的CBTC車站,提高了聯(lián)鎖系統(tǒng)的建模效率與普適性,并且該模板通過(guò)分層建模思想解決模型的狀態(tài)空間爆炸問(wèn)題。(2)針對(duì)CBTC聯(lián)鎖系統(tǒng)的HCPN模型的同步觸發(fā)和并發(fā)性問(wèn)題,本文引入了模型的消息驅(qū)動(dòng)機(jī)制,解決了HCPN模型無(wú)法支持各網(wǎng)絡(luò)層之間并發(fā)行為以及同步觸發(fā)的問(wèn)題。該方法在現(xiàn)有HCPN框架的基礎(chǔ)上,增加消息驅(qū)動(dòng)機(jī)制,能夠?qū)崿F(xiàn)模型中信號(hào)機(jī)、道岔等控制對(duì)象的同步觸發(fā),彌補(bǔ)傳統(tǒng)HCPN的不足。(3)針對(duì)模型轉(zhuǎn)換以及代碼生成問(wèn)題,本文給出了由HCPN模型至B語(yǔ)言符號(hào)的轉(zhuǎn)換方法。該模型轉(zhuǎn)換方法優(yōu)化了模型轉(zhuǎn)換機(jī)制,能夠兼容HCPN多種類型的顏色集。該方法實(shí)現(xiàn)HCPN模型轉(zhuǎn)換至B抽象機(jī)的轉(zhuǎn)換,生成的B抽象機(jī)能夠通過(guò)Atelier B軟件的模型驗(yàn)證,為代碼的自動(dòng)生成提供了保證。(4)針對(duì)單一形式化建模方法的不足之處,本文提出了一種融合基于函數(shù)的建模方法與基于邏輯的建模方法的組合建模方法。該建模方法克服了單一HCPN建模不能反映時(shí)間的問(wèn)題,使得模型更易于發(fā)現(xiàn)系統(tǒng)設(shè)計(jì)中的錯(cuò)誤、不一致性、模糊性和不完備性。將時(shí)間自動(dòng)機(jī)的建模方法運(yùn)用到CBTC聯(lián)鎖系統(tǒng)模板中,增強(qiáng)了聯(lián)鎖模板的通用性。
[Abstract]:As the security key equipment of communication Based Train control system based on communication, the interlocking system is a typical complex security demanding system with complex structure, complex function logic and high integration of hardware and software. How to ensure the correctness and security of interlocking system and find a set of comprehensive and effective modeling and verification methods has become an urgent problem in CBTC system. In recent years, the formal method based on strict mathematical definition has more and more advantages. It can not only describe the structure and function of the system accurately and clearly, but also verify the characteristics of the system. It has become an important theoretical method for modeling and verification of CBTC interlocking systems. Based on this, aiming at the key problems of formal modeling and verification of CBTC interlocking system, this paper studies the reusability of the model, concurrency, transformation method and combinatorial formalization method. The main achievements and innovations of this paper are as follows: (1) in view of the complex state space of CBTC interlocking system model and the huge cost of repeated component model, this paper proposes and implements a CBTC interlocking system model template based on layered colored Petri net. The template belongs to a hierarchical parameterized model, which has strong reusability and is suitable for different CBTC stations. It improves the efficiency and universality of the interlocking system. The template solves the state space explosion problem of the model by the idea of hierarchical modeling. Aiming at the synchronous trigger and concurrency of the HCPN model of CBTC interlocking system, this paper introduces the message-driven mechanism of the model. It solves the problem that the HCPN model can not support concurrent behavior and synchronous trigger among different network layers. Based on the existing HCPN framework, the method adds message-driven mechanism, which can realize synchronous trigger of control objects such as signal generator and switch in the model, and make up the deficiency of traditional HCPN.) aiming at the problem of model transformation and code generation, the method aims at the problem of model transformation and code generation. In this paper, the transformation method from HCPN model to B language symbol is given. The model transformation method optimizes the model transformation mechanism and can be compatible with various color sets of HCPN. This method realizes the conversion of HCPN model to B abstract machine. The generated B abstract machine can be verified by the model of Atelier B software, which can guarantee the automatic generation of code. In this paper, a combination modeling method based on function and logic is proposed. This method overcomes the problem that single HCPN modeling can not reflect time, and makes it easier for the model to find errors, inconsistency, fuzziness and incompleteness in system design. The modeling method of time automata is applied to the CBTC interlocking system template, which enhances the generality of interlocking template.
【學(xué)位授予單位】：中國(guó)鐵道科學(xué)研究院
【學(xué)位級(jí)別】：博士
【學(xué)位授予年份】：2017
【分類號(hào)】：U284.48

【相似文獻(xiàn)】

相關(guān)期刊論文 前10條

1 馬永鴻 ,李紹斌 ,劉明云;運(yùn)輸演練聯(lián)鎖系統(tǒng)落成[J];鐵道運(yùn)輸與經(jīng)濟(jì);2003年07期

2 ;荷蘭鐵路將升級(jí)其聯(lián)鎖系統(tǒng)[J];鐵路技術(shù)創(chuàng)新;2003年04期

3 張?zhí)熨F;馬建忠;;大型氨廠聯(lián)鎖系統(tǒng)分析及改造設(shè)想[J];昆明工學(xué)院學(xué)報(bào);1993年06期

4 李紹斌,蔣大明;鐵路運(yùn)輸沙盤(pán)綜合演練聯(lián)鎖系統(tǒng)的設(shè)計(jì)和實(shí)現(xiàn)[J];中國(guó)鐵路;2005年06期

5 杜軍威;徐中偉;;聯(lián)鎖系統(tǒng)形式化模型的安全性評(píng)估[J];微電子學(xué)與計(jì)算機(jī);2007年08期

6 張福新;杜玉越;;改進(jìn)的最小割集生成算法與聯(lián)鎖系統(tǒng)模型的安全性測(cè)試[J];計(jì)算機(jī)應(yīng)用研究;2009年08期

7 剛建雷;張玲;胡燕來(lái);;聯(lián)鎖系統(tǒng)顯示部件抗干擾性能改進(jìn)[J];鐵道通信信號(hào);2013年S1期

8 李裕熊,寧欣全,李玨忻,吳璨,吳熹,王祥訓(xùn);合肥國(guó)家同步輻射實(shí)驗(yàn)室人身輻射安全聯(lián)鎖系統(tǒng)[J];輻射防護(hù);1992年01期

9 胡天畏;高壓開(kāi)關(guān)聯(lián)鎖系統(tǒng)的新發(fā)展[J];高壓電器;1982年04期

10 吳靖民,雷傳蘅;加速器聯(lián)鎖系統(tǒng)設(shè)計(jì)和運(yùn)行中一個(gè)值得注意的問(wèn)題——高頻引起的 X 射線[J];輻射防護(hù);1987年01期

相關(guān)重要報(bào)紙文章 前3條

1 本報(bào)記者 陳其玨;中國(guó)自動(dòng)化資本開(kāi)支1.2億元擬繼續(xù)并購(gòu)[N];上海證券報(bào);2008年

2 北京和利時(shí)系統(tǒng)工程股份有限公司交通信息系統(tǒng)部 于力明 王偉;HS2000 VSI系統(tǒng)在鐵路信號(hào)聯(lián)鎖系統(tǒng)中的應(yīng)用[N];中國(guó)計(jì)算機(jī)報(bào);2004年

3 記者 宋冰;正常的動(dòng)車信號(hào)系統(tǒng)應(yīng)該怎樣工作？[N];第一財(cái)經(jīng)日?qǐng)?bào);2011年

相關(guān)博士學(xué)位論文 前3條

1 于瀟;CBTC聯(lián)鎖系統(tǒng)的形式化建模與驗(yàn)證方法研究[D];中國(guó)鐵道科學(xué)研究院;2017年

2 魏文軍;基于Agent的全電子智能分布式應(yīng)急聯(lián)鎖系統(tǒng)研究[D];蘭州交通大學(xué);2015年

3 何濤;軌道交通全電子化聯(lián)鎖系統(tǒng)安全技術(shù)研究與系統(tǒng)分析[D];蘭州交通大學(xué);2014年

相關(guān)碩士學(xué)位論文 前10條

1 吳艾玲;城市軌道交通聯(lián)鎖系統(tǒng)接口技術(shù)與安全性研究[D];蘭州交通大學(xué);2015年

2 田澤方;城軌聯(lián)鎖系統(tǒng)中進(jìn)路控制邏輯的自動(dòng)設(shè)計(jì)與實(shí)現(xiàn)[D];西南交通大學(xué);2016年

3 袁晴;基于SCADE的聯(lián)鎖邏輯建模與仿真[D];西南交通大學(xué);2016年

4 雷貝貝;基于SCADE的城軌正線聯(lián)鎖系統(tǒng)研究[D];西南交通大學(xué);2017年

5 廖亮;電子聯(lián)鎖系統(tǒng)安全計(jì)算平臺(tái)的研究與實(shí)現(xiàn)[D];北京交通大學(xué);2008年

6 張重;城市軌道交通聯(lián)鎖系統(tǒng)可靠性及安全性分析研究[D];蘭州交通大學(xué);2014年

7 張?jiān)?鐵路信號(hào)聯(lián)鎖系統(tǒng)安全規(guī)范的形式化描述與驗(yàn)證方法[D];北京交通大學(xué);2013年

8 馬殙;鐵路信號(hào)電子聯(lián)鎖系統(tǒng)研究[D];北京交通大學(xué);2008年

9 陳曉偉;新型分布式計(jì)算機(jī)聯(lián)鎖系統(tǒng)的研究與設(shè)計(jì)[D];蘭州交通大學(xué);2009年

10 吳永成;基于全電子執(zhí)行單元的車站應(yīng)急聯(lián)鎖系統(tǒng)方案的研究[D];蘭州交通大學(xué);2013年

，

本文編號(hào)：1809485