摘要

测试模型是高铁信号系统安全关键功能测试用例编制的重要基础,针对高铁信号系统安全关键功能测试建模过程中描述信号系统领域特征不够全面的问题,提出时间状态机测试建模理论和测试用例生成方法.分析高铁信号系统测试建模的特点,提出信号系统安全关键功能测试模型的建模需求;以有限状态机理论为研究基础,结合功能逻辑和时钟约束提出时间状态机建模方法,采用Z规格说明语言给出时间状态机的形式化定义;将时间状态机转换为时间自动机,证明转换之间的一致性,并基于时间自动机的测试理论自动生成测试用例,再以计算机联锁系统中的道岔转换功能为例,建立时间状态机测试模型并生成测试用例.最后,将两种方法生成的测试案例进行对比,结果表明:在功能逻辑方面,基于时间状态机建模方法生成的测试案例100%地覆盖了基于时间自动机建模方法生成的测试案例,并新增了16条具有时钟约束的测试案例,能够满足高铁信号系统安全关键功能测试建模的需求.