基于UML和TA的RBC系統(tǒng)形式化建模與分析.pdf

1、RBC(Radio Block Center,無(wú)線閉塞中心)是CTCS(Chinese Train Control System Level,中國(guó)列車(chē)控制系統(tǒng)等級(jí))3級(jí)列控系統(tǒng)中保障列車(chē)安全可靠運(yùn)行的關(guān)鍵設(shè)備，其根據(jù)從地面設(shè)備收到的信息數(shù)據(jù)以及通過(guò) GSM-R(Global System for Mobile Communications–Railway,全球數(shù)字鐵路移動(dòng)通信系統(tǒng))網(wǎng)絡(luò)與車(chē)載系統(tǒng)進(jìn)行連續(xù)雙向的交互信息生成MA(Movem

2、ent Authority,行車(chē)許可)來(lái)控制列車(chē)可靠行駛，從而保證了列車(chē)在運(yùn)行線路上安全運(yùn)行。RBC具有苛刻的實(shí)時(shí)性要求，能否滿足此要求直接影響CTCS-3級(jí)列控系統(tǒng)安全、可靠、高效和精確地控制列車(chē)。保證 RBC系統(tǒng)的可靠工作和實(shí)時(shí)性要求，必須保證指導(dǎo)列控系統(tǒng)設(shè)計(jì)的需求規(guī)范和設(shè)計(jì)技術(shù)規(guī)范中不存在任何缺陷，否則都有可能將潛在的風(fēng)險(xiǎn)演變成系統(tǒng)的失效從而導(dǎo)致安全事故的發(fā)生。因此，對(duì)相應(yīng)的規(guī)范建模驗(yàn)證將成為保證其正確合理的有效手段。
　　

3、本文以 CTCS-3列控系統(tǒng)需求規(guī)范為背景，采用半形式化方法 UML(Unified Modeling Language,統(tǒng)一建模語(yǔ)言)和形式化方法時(shí)間自動(dòng)機(jī)相結(jié)合的方法，對(duì)等級(jí)轉(zhuǎn)換和RBC切換兩個(gè)運(yùn)營(yíng)場(chǎng)景進(jìn)行建模驗(yàn)證，保證RBC控車(chē)的實(shí)時(shí)性和安全性要求。首先，對(duì)CTCS-3級(jí)列控系統(tǒng)需求規(guī)范和設(shè)計(jì)技術(shù)方案中的兩個(gè)場(chǎng)景過(guò)程進(jìn)行分析，并根據(jù)時(shí)間特征將各場(chǎng)景劃分為若干模塊；其次，根據(jù)系統(tǒng)實(shí)時(shí)性和信息動(dòng)態(tài)交互等要求，使用UML中擴(kuò)展了時(shí)間特征

4、的順序圖和定時(shí)圖對(duì)每一個(gè)子模塊進(jìn)行建模；再次，利用從UML順序圖到時(shí)間自動(dòng)機(jī)的轉(zhuǎn)換規(guī)則，將建立的UML順序圖和定時(shí)圖模型無(wú)差別的轉(zhuǎn)化為時(shí)間自動(dòng)機(jī)子模型；最后，根據(jù)時(shí)間自動(dòng)機(jī)積的原理將各獨(dú)立的時(shí)間自動(dòng)機(jī)子模型合并成系統(tǒng)的時(shí)間自動(dòng)機(jī)整體網(wǎng)絡(luò)模型，并采用 UPPAAL驗(yàn)證工具對(duì)已有模型仿真得到狀態(tài)遷移圖，利用從規(guī)范中提煉出的BNF(Backus Normal Form,巴科斯范式)驗(yàn)證語(yǔ)句，逐一驗(yàn)證整體網(wǎng)絡(luò)模型中系統(tǒng)的實(shí)時(shí)和安全等性質(zhì)，最終達(dá)