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

Formal Modeling and Verification of CTCS-N Level Conversion Scenarios

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

     

    Abstract: 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.Constructing a model to meet the functional and performance requirements of the system could ensure the safe and efficient operation of the train on the line, so a formal modeling and verification method based on timed automata is proposed 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 corresponding 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.

     

/

返回文章
返回