高铁信号系统安全关键功能测试建模方法

Testing Modeling Method for Safety Critical Function of High-Speed Railway Signal System

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

Testing model is an important basis to create the test cases of safety critical function of high-speed railway signal system.To solve the problem that the characteristics of signal system are not fully represented in the modeling process of safety critical function test of high-speed railway signal system,the modeling theory of timed finite state machine(TFSM)and test case generation method are proposed.The characteristics in the test modeling of high-speed railway signal system is analyzed,and the modeling requirements are put forward.Then,based on the theory of finite state machine,a modeling method of TFSM is proposed by utilizing functional logic and clock constraints,and its formal definition is established with Z notation.Further,the TFSM is transformed into timed automata,which can prove the consistency between them,and test cases are automatically generated with timed automata based testing theory.The switch conversion function of the computer interlocking system is used as an example to build the testing model of TFSM and generate the test cases.The result shows that compared with the test cases generated by timed automata,in terms of functional logic,the test cases generated by TFSM can fully cover those generated by timed automata,and add 16 more test cases with clock constraints,showing that TFSM can meet the testing modeling requirements for the safety critical function of high-speed railway signal system.