發(fā)布時(shí)間：2020-05-15 14:35

【摘要】：計(jì)算機(jī)聯(lián)鎖系統(tǒng)是鐵路控制的核心系統(tǒng)之一,是保障鐵路運(yùn)輸安全的重要一環(huán)。作為典型的安全苛求系統(tǒng),計(jì)算機(jī)聯(lián)鎖軟件的設(shè)計(jì)與開發(fā)應(yīng)嚴(yán)格地按照相關(guān)規(guī)定和高行業(yè)標(biāo)準(zhǔn)進(jìn)行。隨著鐵路系統(tǒng)的快速發(fā)展,在聯(lián)鎖軟件開發(fā)的需求分析階段通過形式化的驗(yàn)證找出存在的問題,對保證鐵路運(yùn)輸系統(tǒng)的安全高效運(yùn)行有著重要意義。然而直接采用形式化方法有著對專業(yè)知識要求高、使用難度大和建模效率低下等缺點(diǎn),因此在站場的規(guī)模與復(fù)雜度不斷提高的今天,需要開發(fā)一種更加高效便捷的聯(lián)鎖軟件形式化驗(yàn)證方法用以保障其正確性。UML(Unified Modeling Language,統(tǒng)一建模語言)如今被廣泛應(yīng)用于軟件開發(fā)領(lǐng)域的各個(gè)階段,它通過多個(gè)視圖結(jié)合能夠準(zhǔn)確全面地從不同角度描述一個(gè)系統(tǒng),然而其作為一種半形式化的語言不能提供有效的自動分析與驗(yàn)證方法。NuSMV(New Symbolic Model Verifier,符號模型驗(yàn)證器)是一種高效成熟的形式化驗(yàn)證工具,若能夠通過UML建立聯(lián)鎖系統(tǒng)模型,再將之轉(zhuǎn)化為形式化的NuSMV模型并對其進(jìn)行驗(yàn)證,則可以通過間接的方式實(shí)現(xiàn)降低對聯(lián)鎖系統(tǒng)形式化建模與驗(yàn)證的難度與提高效率的目的。針對上述問題,本文提出一種UML與NuSMV相結(jié)合的計(jì)算機(jī)聯(lián)鎖系統(tǒng)形式化驗(yàn)證的方法。首先分析聯(lián)鎖系統(tǒng)的框架結(jié)構(gòu)與進(jìn)路控制中每一階段的需求,并針對進(jìn)路選擇階段提出了一種基于坐標(biāo)與站場拓?fù)涞倪M(jìn)路搜索算法,以一個(gè)標(biāo)準(zhǔn)站場為例利用UML類圖、狀態(tài)圖與順序圖這三種視圖建立聯(lián)鎖控制邏輯的需求模型。其次分析對比UML模型與NuSMV形式化模型在結(jié)構(gòu)和語義上的關(guān)聯(lián),并結(jié)合設(shè)備間相互制約的特點(diǎn)制定了一套UML模型到NuSMV模型的轉(zhuǎn)換規(guī)則。然后根據(jù)此規(guī)則在C#環(huán)境下編寫了相應(yīng)的模型轉(zhuǎn)換程序,完成了UML模型到NuSMV模型的批量自動轉(zhuǎn)換。最后,分析與提取計(jì)算機(jī)聯(lián)鎖系統(tǒng)需遵循的相關(guān)技術(shù)規(guī)范,應(yīng)用CTL(Computation Tree Logic,計(jì)算樹邏輯)表達(dá)式描述聯(lián)鎖模型應(yīng)滿足的一些性質(zhì),并將其作為驗(yàn)證語句輸入至NuSMV驗(yàn)證器當(dāng)中完成對計(jì)算機(jī)聯(lián)鎖系統(tǒng)模型的驗(yàn)證工作。驗(yàn)證結(jié)果表明:該方法能夠?qū)崿F(xiàn)高效準(zhǔn)確地驗(yàn)證聯(lián)鎖系統(tǒng)需求的正確性,且能夠舉出反例從而修正可能出現(xiàn)的錯(cuò)誤,為計(jì)算機(jī)聯(lián)鎖系統(tǒng)需求模型的正確性驗(yàn)證提供一種新思路。
【圖文】：

- 7 -圖 2.1 UML 模型的構(gòu)成示意圖L 模型圖構(gòu)成的內(nèi)容分為以下三項(xiàng)：事物成實(shí)際系統(tǒng)的主要內(nèi)容進(jìn)行抽象，是構(gòu)成 UML 模型的基本單元。UML 中物：構(gòu)建事物用于描述模型的靜態(tài)基本元素或概念，如類與接口等；行為當(dāng)中事物間的交互與事物自身的狀態(tài)轉(zhuǎn)變這一類動態(tài)部分；分組事物劃分構(gòu)；注釋事物負(fù)責(zé)對模型中內(nèi)容的解釋。關(guān)系事物之間存在何種關(guān)聯(lián)，關(guān)系的類型有如下四種：依賴：對于一個(gè)獨(dú)立的事物而言，若它的狀態(tài)發(fā)生變化，則依賴于它的相樣變化。

基于UML-NuSMV 的聯(lián)鎖軟件形式化建模與驗(yàn)證一種有效的解決方案。檢測是一種基于時(shí)態(tài)邏輯的形式化驗(yàn)證方法，驗(yàn)證系統(tǒng)時(shí)其核心的關(guān)時(shí)態(tài)性質(zhì)的變化�；�于模型檢測方法的主要內(nèi)容分為三個(gè)部分，，如圖建立系統(tǒng) S 的抽象模型 M，通過一種特定的數(shù)學(xué)語言邏輯對系統(tǒng) S 的模式進(jìn)行描述；第二步是建立性質(zhì)規(guī)約，即根據(jù)系統(tǒng) S 應(yīng)完成的功能過公式對其進(jìn)行表達(dá)，使其成為系統(tǒng)的約束性質(zhì)ψ；第三步是形式化模型M進(jìn)行狀態(tài)空間的檢測，驗(yàn)證其在所有狀態(tài)中是否都能夠滿足約M|=ψ，若模型中存在不能滿足該約束性質(zhì)的狀態(tài)，則將其列出以供修
【學(xué)位授予單位】：蘭州交通大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2018
【分類號】：U284.362

【相似文獻(xiàn)】

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

1 張樹群;;車站計(jì)算機(jī)聯(lián)鎖系統(tǒng)設(shè)備及其使用[J];鄭鐵科技通訊;1999年01期

2 李荊洪;;淺談區(qū)域計(jì)算機(jī)聯(lián)鎖系統(tǒng)[J];鄭鐵科技通訊;2003年01期

3 郭掾龍;;全電子計(jì)算機(jī)聯(lián)鎖系統(tǒng)研究[J];科技經(jīng)濟(jì)導(dǎo)刊;2018年14期

4 李笑涵;殷田一男;楊揚(yáng);;車站計(jì)算機(jī)聯(lián)鎖系統(tǒng)配置信息軟件設(shè)計(jì)[J];鐵路計(jì)算機(jī)應(yīng)用;2016年12期

5 陳建譯;周榮;喬高鋒;王海峰;徐田華;;基于故障數(shù)據(jù)的計(jì)算機(jī)聯(lián)鎖系統(tǒng)壽命預(yù)測方法[J];鐵路計(jì)算機(jī)應(yīng)用;2017年01期

6 陳光;;基于監(jiān)測數(shù)據(jù)的計(jì)算機(jī)聯(lián)鎖系統(tǒng)安全性研究[J];鐵道通信信號;2017年02期

7 李耀;張亞東;郭進(jìn);晏姍;饒暢;曹雅鑫;;鐵路計(jì)算機(jī)聯(lián)鎖系統(tǒng)安全關(guān)鍵軟件的安全性能建模方法[J];中國鐵道科學(xué);2017年02期

8 齊志華;彭陽;徐德龍;;計(jì)算機(jī)聯(lián)鎖系統(tǒng)操作顯示界面優(yōu)化設(shè)計(jì)[J];鐵道通信信號;2017年07期

9 李紅云;;拉薩至林芝鐵路計(jì)算機(jī)聯(lián)鎖系統(tǒng)方案探討[J];高速鐵路技術(shù);2017年05期

10 崔莉;;主流計(jì)算機(jī)聯(lián)鎖系統(tǒng)特點(diǎn)分析[J];無線互聯(lián)科技;2016年12期

相關(guān)會議論文 前10條

1 宋鋼;;關(guān)于移動式計(jì)算機(jī)聯(lián)鎖系統(tǒng)的研究[A];新世紀(jì) 新機(jī)遇 新挑戰(zhàn)——知識創(chuàng)新和高新技術(shù)產(chǎn)業(yè)發(fā)展（上冊）[C];2001年

2 蘆樹晴;;鐵路計(jì)算機(jī)聯(lián)鎖軟件智能測試系統(tǒng)[A];高速鐵路與軌道交通（金融版）[C];2016年

3 段武;;城市軌道交通計(jì)算機(jī)聯(lián)鎖系統(tǒng)[A];中國城市軌道交通新技術(shù)（第三集）[C];2009年

4 潘明;何梅芳;張萍;趙陽;趙永青;;計(jì)算機(jī)聯(lián)鎖安全電子終端及其冗余組態(tài)的研究[A];鐵道科學(xué)技術(shù)新進(jìn)展——鐵道科學(xué)研究院五十五周年論文集[C];2005年

5 陳福濤;張富春;;EI32-JD計(jì)算機(jī)聯(lián)鎖系統(tǒng)常見故障處理[A];河南省鐵道學(xué)會2007年學(xué)術(shù)活動月優(yōu)秀論文選集[C];2007年

6 劉聰芳;;淺談JD-1 A型計(jì)算機(jī)聯(lián)鎖系統(tǒng)原理結(jié)構(gòu)及故障處理[A];第十屆中國科協(xié)年會中部地區(qū)物流產(chǎn)業(yè)體系建設(shè)論壇專輯[C];2008年

7 徐慶寧;;基于HJ04A的鐵路信號計(jì)算機(jī)聯(lián)鎖系統(tǒng)[A];中國計(jì)量協(xié)會冶金分會2009年年會論文集[C];2009年

8 臧永立;;TYJL-Ⅲ型國產(chǎn)容錯(cuò)計(jì)算機(jī)聯(lián)鎖系統(tǒng)研究[A];鐵道科學(xué)技術(shù)新進(jìn)展——鐵道科學(xué)研究院五十五周年論文集[C];2005年

9 張新明;王俊高;;二乘二取二冗余計(jì)算機(jī)聯(lián)鎖系統(tǒng)的結(jié)構(gòu)與安全性分析[A];鐵道科學(xué)技術(shù)新進(jìn)展——鐵道科學(xué)研究院五十五周年論文集[C];2005年

10 陳福濤;張富春;;EI32—JD計(jì)算機(jī)聯(lián)鎖系統(tǒng)常見故障處理[A];河南省鐵道學(xué)會2007年學(xué)術(shù)活動月優(yōu)秀論文集[C];2007年

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

1 王培蓮　本報(bào)記者 白雪;誰在駕馭最先進(jìn)的軌道交通[N];中國青年報(bào);2011年

2 董萍;計(jì)算機(jī)聯(lián)鎖系統(tǒng)上列車運(yùn)行更安全[N];中國教育報(bào);2000年

3 山西省原平市衛(wèi)生學(xué)校 王智麗;計(jì)算機(jī)聯(lián)鎖系統(tǒng)安全可靠性分析[N];山西科技報(bào);2014年

4 通訊員 王冬　朱仁敏;卡斯柯產(chǎn)品通過高新技術(shù)成果轉(zhuǎn)化認(rèn)定[N];人民鐵道;2009年

5 孫清華 李世偉;武廣線信號改造工程首戰(zhàn)告捷[N];山西日報(bào);2000年

6 本報(bào)記者 矯陽;給高鐵安上順風(fēng)耳[N];科技日報(bào);2015年

7 杭慶博;黃礦鐵運(yùn)公司鐵路數(shù)字化改革獲得成功[N];延安日報(bào);2011年

8 記者 唐駿W

本文編號：2665189