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

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

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

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