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

- 7 -圖 2.1 UML 模型的構(gòu)成示意圖L 模型圖構(gòu)成的內(nèi)容分為以下三項：事物成實際系統(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)系的類型有如下四種：依賴：對于一個獨立的事物而言，若它的狀態(tài)發(fā)生變化，則依賴于它的相樣變化。

基于UML-NuSMV 的聯(lián)鎖軟件形式化建模與驗證一種有效的解決方案。檢測是一種基于時態(tài)邏輯的形式化驗證方法，驗證系統(tǒng)時其核心的關(guān)時態(tài)性質(zhì)的變化�；谀Ｐ蜋z測方法的主要內(nèi)容分為三個部分，，如圖建立系統(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)空間的檢測，驗證其在所有狀態(tài)中是否都能夠滿足約M|=ψ，若模型中存在不能滿足該約束性質(zhì)的狀態(tài)，則將其列出以供修
【學(xué)位授予單位】：蘭州交通大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2018
【分類號】：U284.362

【相似文獻(xiàn)】

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

8 記者 唐駿W

本文編號：2665189