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

作     者：高卓凡 何涛 姜飞 吴永成 GAO Zhuofan;HE Tao;JIANG Fei;WU Yongcheng

作者机构：兰州交通大学自动化与电气工程学院兰州730070 甘肃省工业交通自动化工程技术研究中心兰州730070 甘肃省轨道交通信号与控制评测行业技术中心兰州730070 

出 版 物：《兰州交通大学学报》 (Journal of Lanzhou Jiaotong University)

年 卷 期：2024年第43卷第1期

页      面：73-82页

学科分类：08[工学] 082302[工学-交通信息工程及控制] 0823[工学-交通运输工程] 

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

摘      要：新型列车控制系统的车载设备承担更多地面设备的功能,其功能测试主要是以现场测试为主,费时费力,构建满足系统功能与性能需求的模型有助于保证列车在线路上安全、高效地运行,因此针对新型列控系统提出一种基于时间自动机的形式化建模与验证的方法。首先,选取等级转换场景为主要建模场景,提取规范中的功能与性能需求,梳理信息交互图,基于UPPAAL建立车载设备、应答器、临时限速服务器、无线闭塞中心的时间自动机模型;然后,使用模拟器进行模型的仿真,生成对应的消息顺序图;最后,以自动机语言为基础,验证正常模式和故障模式下车载设备转换是否满足要求。验证结果表明:所建立的模型满足等级转换场景的需求,其功能符合对应的技术规范,证明了该形式化建模的可行性,为新型列控系统测试、其他场景或功能的建模与验证提供了参考。