基于统计模型检测的Tc CBTC移动授权建模与分析  

Modeling and Analysis of TcCBTC Movement Authority Based on Statistical Model Checking

作　　者：林俊亭[1] 闵晓琴 LIN Jun-ting;MIN Xiao-qin(School of Automation and Electrical Engineering,Lanzhou Jiaotong University,Lanzhou 730070,China)

机构地区：[1]兰州交通大学自动化与电气工程学院,甘肃兰州730070

出　　处：《控制工程》2023年第5期803-809,821,共8页Control Engineering of China

基　　金：国家自然科学基金资助项目(52162050,61763025);甘肃省自然科学基金资助项目(20JR5RA375)。

摘　　要：基于通信的列车运行控制(communication based train control,CBTC)系统采用车地通信方式使得地面设备极其复杂。随着通信技术的快速发展,以车载为核心的列车运行控制(train-centric communication based train control,TcCBTC)系统采用车车通信方式减少了控制信息的传递环节,将成为城市轨道交通领域的发展方向。移动授权(movementauthority,MA)是决定列车能否以安全间隔运行的直接因素,因此对MA生成过程进行形式化建模与分析,对避免列车碰撞具有重要意义。根据TcCBTC系统架构分析MA生成流程,确定参与功能实现的子系统,并计算出不确定性参数;通过UPPAAL-SMC建立对应的随机混成自动机网络模型;最后采用统计模型检测方法对模型进行定量分析。分析结果表明:置信度为99.95%的情况下,系统在300 ms内成功计算出MA的概率为0.9974124748,为后续TcCBTC系统开发设计提供理论参考。The Communication Based Train Control(CBTC)system uses vehicle-to-ground communication which makes ground equipment extremely complex.With the rapid development of communication technology,the Train-centric CBTC(TcCBTC)system adopting the train-to-train communication to reduce the transmission link of control information will become the direction of the urban rail transit field development.The Movement Authority(MA)is a direct factor that determines whether the train can run at safe intervals,therefore formal modeling and analysis of the MA generation process is of great significance to avoid train collisions.The MA generation process is analyzed according to the TcCBTC system architecture,to determine subsystems involved in the realization of the function,and the uncertainty parameters are calculated;then a corresponding Network of Stochastic Hybrid Automata is established by UPPAAL-SMC.Finally,the Statistical Model Checking method is used to analyze the model quantitatively.The analysis results show that the probability of successful computation of the MA within 300 ms is 0.9974124748 by the system when the confidence level is 99.95%,which provides a theoretical reference for the subsequent development and design of the TcCBTC system.

关 键 词：随机混成自动机 统计模型检测 以车载为核心的列车运行控制 移动授权 

分 类 号：TP391.9[自动化与计算机技术—计算机应用技术] U284.48[自动化与计算机技术—计算机科学与技术]