基于NuSMV和STPA的RBC交接場(chǎng)景安全分析方法研究.pdf

1、中國(guó)列車(chē)運(yùn)行控制系統(tǒng)3級(jí)（Chinese Train Control System Level3，CTCS-3）是中國(guó)高速鐵路的核心裝備，負(fù)責(zé)保障高速鐵路列車(chē)的行車(chē)安全，也是高速鐵路的“神經(jīng)中樞”，其安全性對(duì)于高速鐵路的安全運(yùn)營(yíng)起到了關(guān)鍵的作用。無(wú)線閉塞中心(Radio Block Center，RBC)交接場(chǎng)景是CTCS-3級(jí)列車(chē)運(yùn)行控制系統(tǒng)（簡(jiǎn)稱(chēng)CTCS-3級(jí)列控系統(tǒng)）的重要運(yùn)營(yíng)場(chǎng)景。針對(duì)其特點(diǎn)研究有效的、科學(xué)的安全分析方法，對(duì)于保

2、障高速鐵路的安全具有重要意義。然而，CTCS-3級(jí)列控系統(tǒng)的功能和組件交互之間的關(guān)系錯(cuò)綜復(fù)雜，運(yùn)用傳統(tǒng)的安全分析方法時(shí)會(huì)面臨挑戰(zhàn)。系統(tǒng)理論過(guò)程分析(System-Theoretic Process Analysis，STPA)作為建立在系統(tǒng)理論事故模型(Systems-Theoretic Accident Model and Process，STAMP)基礎(chǔ)上的新技術(shù)，將導(dǎo)致危險(xiǎn)的主要原因歸結(jié)為組件間的異常交互，滿足CTCS-3級(jí)列控系

3、統(tǒng)對(duì)安全分析方法的要求。但是，目前沒(méi)有統(tǒng)一的方法來(lái)描述該模型，而采用自然語(yǔ)言建模又容易受人員表述能力的影響而導(dǎo)致歧義。此外，STPA安全分析主要依靠分析人員人工實(shí)施，其分析結(jié)果的可信度受分析人員經(jīng)驗(yàn)的影響較大。
　　本論文從目前現(xiàn)有的建模與分析方法存在的不足出發(fā)，利用UML統(tǒng)一建模語(yǔ)言的可擴(kuò)展性等優(yōu)點(diǎn)，對(duì)STPA方法中系統(tǒng)分層控制結(jié)構(gòu)模型的構(gòu)建方法進(jìn)行改進(jìn)，并利用NuSMV能自動(dòng)給出反例的特性輔助實(shí)施STPA安全分析過(guò)程。

4、　　主要的內(nèi)容包括:
　　(1)在理解并閱讀了大量國(guó)內(nèi)外文獻(xiàn)研究之后，簡(jiǎn)單介紹目前安全分析方法的研究情況，并針對(duì)不同安全分析方法的優(yōu)點(diǎn)及不足做出對(duì)比和分析，明確現(xiàn)有安全分析方法在列控領(lǐng)域的研究前景。
　　(2)設(shè)計(jì)面向STAMP模型的UML概要文件，擴(kuò)展UML類(lèi)圖和控制反饋消息，針對(duì)STPA方法進(jìn)行擴(kuò)展，從而刻畫(huà)出待分析系統(tǒng)的分層控制結(jié)構(gòu)模型。
　　(3)將上述半形式化的UML模型轉(zhuǎn)化為形式化NuSMV模型，構(gòu)建功能失

5、效描述符號(hào)(Functional Failure Description Symbol，F(xiàn)FDS)和故障模型(Fault Pattern，F(xiàn)P)，對(duì)可能的功能模塊失效進(jìn)行文本描述，并將系統(tǒng)的行為模型與故障模型相整合，形成包含故障集的NuSMV模型。然后，運(yùn)用模型檢驗(yàn)的方法構(gòu)建控制缺陷的分析方法。
　　(4)針對(duì)RBC交接場(chǎng)景的特點(diǎn)，分別從靜態(tài)結(jié)構(gòu)以及動(dòng)態(tài)行為的角度出發(fā)來(lái)描述研究實(shí)例，運(yùn)用UML擴(kuò)展后的概要文件創(chuàng)建實(shí)例中的分層控制結(jié)