CTCS-N等级转换场景形式化建模与验证  

Formal Modeling and Verification of CTCS-N Level Conversion Scenarios

作　　者：高卓凡 何涛 姜飞 吴永成 GAO Zhuofan;HE Tao;JIANG Fei;WU Yongcheng(School of Automation and Electrical Engineering,Lanzhou Jiaotong University,Lanzhou 730070,China;Gansu Research Center of Automation Engineering Technology for Industry&Transportation,Lanzhou 730070,China;Gansu Rail Transit Signal and Control Evaluation Industry Technology Center,Lanzhou 730070,China)

机构地区：[1]兰州交通大学自动化与电气工程学院,兰州730070 [2]甘肃省工业交通自动化工程技术研究中心,兰州730070 [3]甘肃省轨道交通信号与控制评测行业技术中心,兰州730070

出　　处：《兰州交通大学学报》2024年第1期73-82,共10页Journal of Lanzhou Jiaotong University

摘　　要：新型列车控制系统的车载设备承担更多地面设备的功能,其功能测试主要是以现场测试为主,费时费力,构建满足系统功能与性能需求的模型有助于保证列车在线路上安全、高效地运行,因此针对新型列控系统提出一种基于时间自动机的形式化建模与验证的方法。首先,选取等级转换场景为主要建模场景,提取规范中的功能与性能需求,梳理信息交互图,基于UPPAAL建立车载设备、应答器、临时限速服务器、无线闭塞中心的时间自动机模型;然后,使用模拟器进行模型的仿真,生成对应的消息顺序图;最后,以自动机语言为基础,验证正常模式和故障模式下车载设备转换是否满足要求。验证结果表明:所建立的模型满足等级转换场景的需求,其功能符合对应的技术规范,证明了该形式化建模的可行性,为新型列控系统测试、其他场景或功能的建模与验证提供了参考。The onboard equipment of Chinese train control system-new(CTCS-N)undertakes more functions of ground equipment.Its function test of CTCS-N is based on field test,which is time-consuming and laborious.Con-structing a model to meet the functional and performance requirements of the system could ensure the safe and effi-cient operation of the train on the line,so a formal modeling and verification method based on timed automata is pro-posed for CTCS-N.Firstly,the level conversion scenarios is selected as the main modeling scenario,extracting the functional and performance requirements in the specification,and combing the information interaction diagram,the time automata models of onboard equipment,balise,temporary speed restriction server and radio block center are built based on UPPAAL.Finally,based on Backus Naur form(BNF)statements,whether the conversion of onboard equipment in normal mode and fault mode have met the requirements is verified.The validation results show that the model meets the requirements of level conversion scenarios.The system functions in this scenario conform to the cor-responding technical specifications,which proves the feasibility of the formal modeling,and provide reference for modeling and validation of CTCS-N system testing,and other scenarios or functionalities.

关 键 词：新型列控系统 时间自动机 等级转换场景 建模与验证 消息顺序图 

分 类 号：U284.48[交通运输工程—交通信息工程及控制]