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

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

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

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