基于模型的城際鐵路列控系統(tǒng)運營場景仿真與驗證.pdf

1、隨著列車運行控制相關技術的發(fā)展，列控系統(tǒng)不斷融合先進的計算機技術、網(wǎng)絡技術以及通信技術，系統(tǒng)的自動化程度不斷提高、軟硬件規(guī)模不斷擴大，呈現(xiàn)出復雜的系統(tǒng)特性。作為復雜的安全苛求系統(tǒng)，如何確保列控系統(tǒng)的正確性是重要的研究課題。一方面，Simulink/Stateflow支持圖形化建模與仿真，可在系統(tǒng)的前期設計開發(fā)中排除部分安全隱患。另一方面，基于嚴格數(shù)學定義的形式化方法能精確，清晰地描述系統(tǒng)的結(jié)構(gòu)和屬性，已成為保障列控系統(tǒng)安全的重要手段。因

2、此仿真模型輔以形式化技術為列控系統(tǒng)的建模和驗證提供了一種新的思路。
　　本文從城際鐵路列控系統(tǒng)的混成屬性入手，研究列控系統(tǒng)運營場景的建模與驗證，提出了一個集建模、仿真與驗證為一體的保障列控系統(tǒng)安全的方法。主要開展了以下相關工作:
　　(1)針對城際鐵路列控系統(tǒng)的混成屬性，研究了基于Simulink/Stateflow的列控系統(tǒng)運營場景的建模與仿真。建立了城際鐵路列控系統(tǒng)的分層模型;引入場景分析方法描述列控系統(tǒng)中各設備對象的典

3、型功能活動以及信息交互，并給出了列控系統(tǒng)運營場景的建模與仿真流程。
　　(2)基于混成自動機理論，研究了對仿真模型輔以形式化驗證以保障城際鐵路列控系統(tǒng)正確性的方法。方法中對Simulink/Stateflow模型和混成自動機模型的形式化語義進行分析，制定了二者間的模型轉(zhuǎn)換規(guī)則，以保證模型轉(zhuǎn)換過程中模型的一致性，并給出了基于SpaceEx驗證平臺的場景模型的驗證流程。
　　(3)在MATLAB環(huán)境中構(gòu)建了列車自動運行場景的仿真

4、平臺。仿真平臺以真實線路作為底層數(shù)據(jù)驅(qū)動，對模型產(chǎn)生的緊急制動距離與試驗中的真實數(shù)據(jù)進行對比分析;對不同參數(shù)組合情況下的列車行為進行仿真分析，并復現(xiàn)了在實際測試現(xiàn)場發(fā)現(xiàn)的安全隱患。
　　(4)以城際鐵路列控系統(tǒng)典型的列車自動運行場景為案例進行分析，運用提出的模型轉(zhuǎn)換規(guī)則將所建立的列車自動運行場景仿真模型轉(zhuǎn)換為混成自動機模型;在SpaceEx混成系統(tǒng)驗證工具中建立混成自動機模型，并對系統(tǒng)驗證屬性進行驗證分析，證明了論文提出的建模和驗