中文摘要：

高速铁路列车运行控制系统是一个典型的实时系统,如何保证列控系统在时延约束条件下功能实现的正确性至关重要。传统的离线测试方法已广泛用于列控系统功能一致性测试中,然而,随着系统复杂度的提高,物理环境中时延的非确定性制约传统离线测试方法的应用。本文引入＂在线测试＂的概念,利用时间自动机理论对典型场景车载设备的RBC切换过程建模,并定义可观测消息通道将该模型划分为环境和设备两部分,从而借助工具UPPAAL-TRON＂边生成边执行＂测试用例,找出了在非确定性时延下,仿真RBC测试模型与测试需求中不一致的地方。并通过改进测试模型中RBC处理占用参数的设置,实现对RBC切换过程中跨界传递联锁消息时延非确定性的一致性测试。

英文摘要：

As high-speed train control system is a typical real-time system,it is crucial to ensure the functional correctness of the train control system on time delay constraint.With increasing system complexity and interaction,traditional offline testing method,which has been widely used in train control system＇s functions conformance testing,however,has been restricted from further use by the non-determinism of time delay in physical environment.In this paper,the concept of online testing was introduced,where timed automata theory was used to model a typical scenario of RBC handover process of on-board equipment,and observable message channels were defined to divide the model into two parts,the environment and the equipment.Test cases were implemented after being generated by using the tool UPPAAL-TRON,to find out inconsistencies between the RBC simulation test model and the testing requirements under non-deterministic time delay.The non-deterministic delay of crossing interlock messages＇ conformance testing is accomplished using tool UPPAAL-TRON.Inconsistencies are found between system under test and its related testing specification.After modification of the parameters of the occupation function in RBC in the test model,the conformance testing of the non-deterministic time delay of transboundary interlocking message transmission in RBC handover scenario has been realized.