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

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

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

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

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

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