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

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

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

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

【相似文獻】

相關期刊論文 前10條

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

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

3 郭掾龍;;全電子計算機聯鎖系統(tǒng)研究[J];科技經濟導刊;2018年14期

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

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

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

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

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

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

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

相關會議論文 前10條

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

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

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

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

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

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

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

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

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

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

相關重要報紙文章 前10條

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

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

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

4 通訊員 王冬　朱仁敏;卡斯柯產品通過高新技術成果轉化認定[N];人民鐵道;2009年

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

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

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

8 記者 唐駿W

本文編號：2665189