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

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

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

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

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