基于UPPAAL的聯(lián)鎖進(jìn)路控制流程建模與驗(yàn)證.pdf

1、信號(hào)系統(tǒng)是城市軌道交通的主要技術(shù)裝備，它擔(dān)負(fù)著指揮列車(chē)運(yùn)行、保證行車(chē)安全、提高運(yùn)輸效率的重要任務(wù)。計(jì)算機(jī)聯(lián)鎖（CI）又是城市軌道交通信號(hào)系統(tǒng)的重要組成部分，它實(shí)現(xiàn)信號(hào)、道岔與進(jìn)路的制約關(guān)系，從而保證了行車(chē)的安全。城市軌道交通的計(jì)算機(jī)聯(lián)鎖把聯(lián)鎖關(guān)系和ATP功能結(jié)合起來(lái)，不僅邏輯復(fù)雜，而且還增加了許多特殊的功能，對(duì)安全性、可靠性和實(shí)時(shí)性都提出了更高的要求。并且隨著計(jì)算機(jī)技術(shù)的在信號(hào)系統(tǒng)的應(yīng)用，傳統(tǒng)的設(shè)計(jì)、分析和測(cè)試方法已經(jīng)無(wú)法滿(mǎn)足計(jì)算機(jī)聯(lián)鎖

2、的安全需求。為此我們采用形式化的方法對(duì)聯(lián)鎖軟件進(jìn)行安全性設(shè)計(jì)和驗(yàn)證，以此來(lái)保證系統(tǒng)設(shè)計(jì)開(kāi)發(fā)的正確性和安全性。 論文以城市軌道交通計(jì)算機(jī)聯(lián)鎖軟件的核心——進(jìn)路控制過(guò)程為研究重點(diǎn)，根據(jù)安全苛求系統(tǒng)的設(shè)計(jì)要求，提出了聯(lián)鎖軟件設(shè)計(jì)的“V”型框架。論文基于該框架提出的需求分析、系統(tǒng)設(shè)計(jì)、形式化建模、形式化需求分析和驗(yàn)證的總體思路展開(kāi)研究。 本文首先介紹了聯(lián)鎖軟件的基本結(jié)構(gòu)和原理，分析了聯(lián)鎖軟件的功能需求和性能需求，在此基礎(chǔ)上重點(diǎn)分

3、析了聯(lián)鎖的進(jìn)路控制流程，從進(jìn)路的建立到解鎖對(duì)進(jìn)路控制的各個(gè)模塊和消息處理流程進(jìn)行了分析和設(shè)計(jì)。 本文提出了基于時(shí)間自動(dòng)機(jī)對(duì)進(jìn)路控制流程進(jìn)行建模。首先根據(jù)進(jìn)路控制流程的各個(gè)功能模塊分別建立子自動(dòng)機(jī)，對(duì)于進(jìn)路控制中的消息處理單獨(dú)建立時(shí)間自動(dòng)機(jī)模型。最后利用UPPAAL工具建立系統(tǒng)的時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)?；跁r(shí)間自動(dòng)機(jī)的形式化建模，利用有向圖形象地描述系統(tǒng)的邏輯行為，通過(guò)加入時(shí)間約束集描述系統(tǒng)的實(shí)時(shí)性，從而避免了聯(lián)鎖軟件設(shè)計(jì)中的不一致、模糊