基于TCSP的區(qū)域控制器分層建模與驗(yàn)證.pdf

1、城市軌道交通是解決大城市擁堵、方便百姓出行的重要手段之一?；谕ㄐ诺牧熊?chē)自動(dòng)控制系統(tǒng)CBTC(Communication Based Train Control)是保證城市軌道交通行車(chē)安全、高效運(yùn)營(yíng)的系統(tǒng)，區(qū)域控制器ZC(Zone Controller)作為CBTC系統(tǒng)的關(guān)鍵設(shè)備，具有實(shí)現(xiàn)列車(chē)管理、移動(dòng)授權(quán)計(jì)算等安全功能。本文針對(duì)ZC子系統(tǒng)功能的安全驗(yàn)證，傳統(tǒng)仿真、測(cè)試的方法存在操作量大、完備性不強(qiáng)，單一形式化方法難以描述ZC子系統(tǒng)復(fù)雜

2、功能的問(wèn)題，給出了一種基于TCSP(TimedCommunicating Sequential Process)的分層建模與驗(yàn)證方法來(lái)對(duì)ZC子系統(tǒng)安全性驗(yàn)證進(jìn)行了研究。
　　本文采用的分層建模方法是將ZC子系統(tǒng)分為系統(tǒng)層和功能層，層間靠系統(tǒng)數(shù)據(jù)關(guān)聯(lián)，并采用加入時(shí)間機(jī)制的建模方法來(lái)表達(dá)系統(tǒng)的實(shí)時(shí)性，用UML-RT(Unified Modeling Language-Real Time)順序圖形象直觀的描述系統(tǒng)交互層，利用標(biāo)簽遷移系統(tǒng)

3、LTS(Labelled Transition System)，實(shí)現(xiàn)半形式化UML-RT到形式化語(yǔ)言TCSP的轉(zhuǎn)換，結(jié)合內(nèi)部功能處理層的TCSP模型，建立整體的基于TCSP的ZC子系統(tǒng)分層模型，層次清晰、要素明確。在現(xiàn)有的通信順序進(jìn)程驗(yàn)證軟件PAT(Process Analysis Toolkit)上運(yùn)行，基于LTL(Linear Temporal Logic)斷言對(duì)技術(shù)規(guī)范提出的數(shù)據(jù)相關(guān)需求進(jìn)行驗(yàn)證。
　　論文選取任務(wù)啟動(dòng)及正常