基于UML-NuSMV模型的列控系統(tǒng)需求階段的安全分析.pdf

1、在中國的交通運輸體系中，鐵路已經(jīng)成為其中最重要的基礎(chǔ)設(shè)施和最大眾化的交通工具。而列車運行控制系統(tǒng)（簡稱列控系統(tǒng)）是保證列車行車安全和高效運行的關(guān)鍵裝備，是整個鐵路系統(tǒng)的核心技術(shù)。一旦列控系統(tǒng)出現(xiàn)安全性問題，極有可能導致行車中斷，甚至是車毀人亡的災難。因此，在列控系統(tǒng)開發(fā)的早期，即需求階段對系統(tǒng)進行安全分析尤為重要。
　　列控系統(tǒng)的研究采用國際通用的方法——“標準先行”，即先完成系統(tǒng)規(guī)范的制定，然后以此指導后續(xù)的系統(tǒng)開發(fā)。故此，本文

2、對于列控系統(tǒng)需求階段的安全分析是以列控系統(tǒng)需求規(guī)范作為研究對象，并對其描述的系統(tǒng)進行建模分析與形式化驗證，然后建立故障模型進行融合完成安全分析。主要的研究內(nèi)容如下:
　　1、采用統(tǒng)一建模語言(Unified Modeling Language，UML)對列控規(guī)范進行初期建模分析，從系統(tǒng)需求、靜態(tài)結(jié)構(gòu)和動態(tài)行為三個維度抽象出列控系統(tǒng)的主要特征，并對建模語言進行了擴展設(shè)計，增強建模語言的刻畫能力。
　　2、運用轉(zhuǎn)換規(guī)則，將UML

3、模型轉(zhuǎn)換成形式化NuSMV模型，利用形式化技術(shù)完成需求規(guī)范的驗證，奠定后續(xù)安全分析的基礎(chǔ)。提出故障模式的失效符號標記，產(chǎn)生融合故障模型的形式化模型，完成本文提出的基于UML-NuSMV模型的列控系統(tǒng)需求階段安全分析的工作。
　　3、為列控系統(tǒng)需求階段的屬性驗證和安全分析開發(fā)了支持工具:RMTool。該工具實質(zhì)是一個插件，集成到（Rational Software Architect，RSA）平臺，通過相關(guān)的接口與形式化工具、UML