基于混成自動(dòng)機(jī)的ZC子系統(tǒng)安全的驗(yàn)證方法研究.pdf

1、近年來，隨著城市化進(jìn)程的加速，城市軌道交通業(yè)已經(jīng)成為市內(nèi)交通的首選，用以緩解交通擁堵的情況。結(jié)合了通信技術(shù)，計(jì)算機(jī)技術(shù)與自動(dòng)控制技術(shù)的基于通信的列車控制系統(tǒng)(Communication Based Train Control，CBTC)是我國使用的城市軌道交通控制系統(tǒng)。作為一個(gè)安全苛求系統(tǒng)和復(fù)雜系統(tǒng)，在完成系統(tǒng)設(shè)計(jì)開發(fā)之后驗(yàn)證系統(tǒng)性質(zhì)是否符合設(shè)計(jì)需求和尋找安全隱患是一項(xiàng)重要的任務(wù)?，F(xiàn)階段對(duì)于系統(tǒng)安全的分析驗(yàn)證主要利用傳統(tǒng)的故障樹等經(jīng)典安

2、全分析方法以及基于形式化模型的系統(tǒng)安全驗(yàn)證。本文從CBTC系統(tǒng)混成特性角度，利用線性混成自動(dòng)機(jī)模型對(duì)ZC子系統(tǒng)功能建模，驗(yàn)證ZC子系統(tǒng)是否滿足設(shè)計(jì)需求及行車安全。
　　論文從CBTC系統(tǒng)原理及結(jié)構(gòu)入手，總結(jié)出實(shí)時(shí)特性、安全特性、混合特性和并發(fā)特性四種CBTC系統(tǒng)具有的明顯特征。目前對(duì)于實(shí)時(shí)與并發(fā)特性的研究有利用通信順序進(jìn)程與時(shí)間自動(dòng)機(jī)形式化方法建立系統(tǒng)模型并進(jìn)行驗(yàn)證。針對(duì)ZC子系統(tǒng)混成特性建模進(jìn)行形式化驗(yàn)證的研究較少，混成特性關(guān)系

3、到系統(tǒng)控制列車運(yùn)行安全問題。本文提出利用線性混成自動(dòng)機(jī)形式化方法對(duì)ZC子系統(tǒng)進(jìn)行建模分析與性質(zhì)驗(yàn)證。
　　文章選取擴(kuò)展能力較強(qiáng)的統(tǒng)一建模語言(Unified Modeling Language，UML)對(duì)系統(tǒng)進(jìn)行描述，利用元素構(gòu)造型、標(biāo)記值和約束的UML擴(kuò)展方式對(duì)UML順序圖進(jìn)行了時(shí)間與變量方面擴(kuò)展，表現(xiàn)系統(tǒng)的實(shí)時(shí)、并發(fā)和混合特性。根據(jù)模型轉(zhuǎn)換理論，將擴(kuò)展后的UML順序圖轉(zhuǎn)換為線性混成自動(dòng)機(jī)。通過制定嚴(yán)格的轉(zhuǎn)換規(guī)則，保證模型轉(zhuǎn)換過