基于時間自動機(jī)的ZC子系統(tǒng)建模與驗(yàn)證.pdf

1、近年來，隨著城市化進(jìn)程的加速，城市軌道交通迅速發(fā)展，基于通信的列車運(yùn)行控制（Communication Based Train Control，CBTC）系統(tǒng)逐漸被廣泛使用。區(qū)域控制器(Zone Controller，ZC)作為CBTC系統(tǒng)地面核心子系統(tǒng)，通過與其它設(shè)備間的交互通信，實(shí)時的為列車計算移動授權(quán)(Movement Authority，MA)信息，實(shí)現(xiàn)列車的間隔控制。ZC子系統(tǒng)作為一個典型的實(shí)時系統(tǒng)，其行為狀態(tài)的遷移過程中，邏

2、輯性和時序性的正確對保障系統(tǒng)安全具有重要意義。因此，為了進(jìn)一步確保ZC子系統(tǒng)能夠安全運(yùn)行實(shí)現(xiàn)其功能，本文提出了一種基于時間自動機(jī)的ZC子系統(tǒng)建模與驗(yàn)證方法，通過對系統(tǒng)進(jìn)行建模，從邏輯性和時序性兩方面驗(yàn)證分析系統(tǒng)運(yùn)行時是否滿足安全需求。
　　本文首先對ZC子系統(tǒng)的特點(diǎn)進(jìn)行了分析，并采用層次化結(jié)構(gòu)思想把ZC子系統(tǒng)分為系統(tǒng)設(shè)備層和功能邏輯層。其次，根據(jù)UML擴(kuò)展方式，針對ZC子系統(tǒng)特點(diǎn)，把順序圖元模型在時鐘約束和變量兩方面做了合理擴(kuò)展，

3、使其能夠更充分地描述系統(tǒng)在交互過程中的邏輯性和時序性。然后，根據(jù)模型轉(zhuǎn)化理論，在確保模型轉(zhuǎn)換過程一致性的基礎(chǔ)上，制定合理的轉(zhuǎn)換規(guī)則，把半形式化擴(kuò)展順序圖轉(zhuǎn)化為形式化的時間自動機(jī)模型。并對形式化驗(yàn)證方法分類做了概述，闡述了時間自動機(jī)模型驗(yàn)證工具UPPAAL的基本結(jié)構(gòu)和功能。在此基礎(chǔ)上，分析了LTL公式到BNF公式的邏輯語義轉(zhuǎn)換形式。
　　本文最后選取MA回撤和列車跨越ZC邊界區(qū)域兩個場景案例進(jìn)行分析，分別建立時間自動機(jī)模型，并在UP