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

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

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

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