计算机应用研究2013，Vol.30Issue(2)：443-446,453,5.DOI:10.3969/j.issn.1001-3695.2013.02.034
CTCS-3列控系统RBC切换的形式化建模、分析与验证
Formal modeling, analysis and verification of RBC handover for CTCS-3 train control system
摘要
Abstract
In order to understand the influence of train speed, RBC handover time, etc. on the quality of RBC handover, and clarify the misunderstanding on the safety of RBC handover protocols, it chosen the stochastic Petri net as the formal description tool to establish the RBC handover model of Chinese train control system level 3. By theoretical analysis and simulations, verified the reliability, safety and rationality of RBC handover protocol A, B under the condition of high-speed train running in RBC handover area with different speed. Because the interruption interval had been taken into account by the RBC handover protocol B, as a redundant measure of protocol A, it has no safety problem in terms of the success probability of RBC handover, but the reduction of RBC handover efficiency has a negative impact on the efficiency of train operation. On the other hand, as the train speed increases, the reliability of RBC handover will go down. To keep the reliability meeting with requirements of the related standards, increasing the overlapping coverage areas between the adjacent RBCs, radio-field strength and the time margin of train headway can be taken into account.关键词
CTCS-3列控系统/RBC切换/通信协议/形式化建模/Petri网/分析与验证Key words
Chinese train control system level 3/ radio block center( RBC) handover/ communication protocols/ formal modeling/ Petri net/ analysis and verification分类
信息技术与安全科学引用本文复制引用
潘登,郑应平..CTCS-3列控系统RBC切换的形式化建模、分析与验证[J].计算机应用研究,2013,30(2):443-446,453,5.基金项目
国家自然科学基金资助项目(61174183) （61174183）
