基于UPPAAL的CBTC系統(tǒng)數(shù)據(jù)驗證的研究.pdf

1、基于通信的列車控制（Communication Based Train Control，CBTC）系統(tǒng)是保證列車運行安全、提高運輸效率的安全苛求系統(tǒng)。CBTC各子系統(tǒng)依靠配置數(shù)據(jù)來定義系統(tǒng)的功能，數(shù)據(jù)作為系統(tǒng)核心組成部分，其正確性是CBTC系統(tǒng)安全連續(xù)運行的重要保證，如何保證數(shù)據(jù)的正確性，尋找一種有效的研究方法對整個CBTC系統(tǒng)具有非常重要的意義?；趪栏駭?shù)學定義的形式化方法不僅能精確、清晰地描述系統(tǒng)結構和相關特性，而且能對特性進行驗證

2、，本文采用形式化的方法對CBTC系統(tǒng)數(shù)據(jù)進行驗證，以此來保證系統(tǒng)數(shù)據(jù)的正確性。
　　首先，論文分析了CBTC系統(tǒng)結構組成與數(shù)據(jù)特點，根據(jù)安全苛求系統(tǒng)和CBTC系統(tǒng)的具體需求，結合時間自動機理論和模型分析驗證工具UPPAAL，提出了基于UPPAAL的CBTC系統(tǒng)數(shù)據(jù)驗證的方法，并設計了CBTC系統(tǒng)數(shù)據(jù)驗證的具體建模方法和驗證流程。
　　然后，論文在前述理論基礎和流程設計的基礎上，按照CBTC系統(tǒng)數(shù)據(jù)的形式化驗證機制，先后對CB

3、TC系統(tǒng)的數(shù)據(jù)組成與描述方式進行了分析和深入研究。圍繞CBTC系統(tǒng)數(shù)據(jù)的性質和特點，總結了CBTC系統(tǒng)所需的基礎線路數(shù)據(jù)、軌旁設備數(shù)據(jù)以及區(qū)域功能數(shù)據(jù)，得到CBTC系統(tǒng)數(shù)據(jù)驗證的策略，從值域關系、參照關系和邏輯關系三個角度建立了數(shù)據(jù)約束集合，并根據(jù)這些數(shù)據(jù)約束條件對CBTC系統(tǒng)數(shù)據(jù)驗證體系進行建模，形成一種數(shù)據(jù)的自動化驗證方法。先將系統(tǒng)數(shù)據(jù)抽象成帶有狀態(tài)的時間自動機模型，然后把數(shù)據(jù)約束條件以數(shù)學公式和邏輯語言的方式加以描述，并針對CBT