軌旁系統(tǒng)安全性的形式化驗證.pdf

1、軌旁系統(tǒng)是列車控制系統(tǒng)中安全級別最高的子系統(tǒng)之一，一旦出現(xiàn)問題，將可能造成列車乘客的人身和財產(chǎn)安全的損失，導(dǎo)致無法挽回的后果。因此，如何保障軌旁系統(tǒng)的安全性是目前亟待解決的問題。模型檢測是現(xiàn)有的形式化驗證的方法之一，主要通過遍歷系統(tǒng)空間來實現(xiàn)系統(tǒng)的驗證，從而能確保系統(tǒng)符合相應(yīng)的安全需求。
　　然而，由于軌旁系統(tǒng)的物理環(huán)境和系統(tǒng)行為都十分復(fù)雜，隨著模型檢測方法逐步應(yīng)用于軌旁系統(tǒng)，出現(xiàn)了系統(tǒng)的狀態(tài)空間超出驗證工具的極限，從而導(dǎo)致驗證失

2、敗的問題。隨著驗證工作的進(jìn)一步深入，我們在軌旁系統(tǒng)驗證的過程中發(fā)現(xiàn)了兩種基本情況：一是某些安全需求只與輸入變量中的一部分相關(guān)，因此可以采用投影的方法控制系統(tǒng)的復(fù)雜度。二是某些變量之間存在著因果關(guān)系，因此可以對變量間的因果關(guān)系進(jìn)行分析，嘗試找出降低系統(tǒng)復(fù)雜度的方法。
　　本文提出了一種基于投影和因果關(guān)系的狀態(tài)空間約簡方法。首先，本文用問題圖描繪了軌旁系統(tǒng)，接著分析了軌旁系統(tǒng)和它的驗證系統(tǒng)之間的關(guān)系，從而得到了軌旁驗證系統(tǒng)的問題圖。之

3、后，本文選用了安全子屬性作為投影維度，定義投影算子，并在此基礎(chǔ)上對原軌旁驗證系統(tǒng)進(jìn)行投影，從而得到了更小的驗證模塊、運行環(huán)境和安全需求。之后，本文分析了設(shè)備內(nèi)部變量之間存在的各種因果關(guān)系，提出根據(jù)因果關(guān)系對變量進(jìn)行約簡的方法，從而減少驗證過程中實際使用到的變量個數(shù)，進(jìn)一步降低了驗證時產(chǎn)生的狀態(tài)空間。
　　論文最后結(jié)合實際工程中采集的數(shù)據(jù)，展示了軌旁系統(tǒng)完整的化簡和驗證過程。我們以 iCMTC系統(tǒng)中的iZC為待驗證系統(tǒng)，采集了一條地