The Research On Mutation Testing Method Of Chinese Train Control System Level 3 Based On Timed Automata

As the high-speed train control system is a typical safety-critical system, once the train control system fails, it will cause serious harms on human lives and property. So it is very important to guarantee the correctness and safety of the system. Testing is a significant technical method to ensure the safety and reliability of high-speed train control system. For a long time, to generate test cases and to ensure its completeness are key points in the testing of train control system, which have a direct bearing on efficiency and quality of the testing. However, it is a thorny problem to evaluate the test cases’quality and ability of detecting errors, which relates to the evaluation of test case set’s completeness. Methods that can solve this problem are needed.Mutation testing, which can simulate most kinds of fault models, provides an alternative or complementary method of measuring test sufficiency and gives a direct and quantitative index to evaluate the completeness of test cases. At the same time, test case set can be revised and supplemented by mutation analysis to raise its completeness. In this paper, mutation testing method based on Timed Automata (TA) is introduced. Firstly, the models of the typical scenarios in the Chinese Train Control System (CTCS) based on TA are built according to the specifications of CTCS. Secondly, some researches on test case set based on the model and evaluation of its completeness are executed. Finally, more sufficient test case set is generated by constantly looking for test cases that have stronger fault detection ability.The main contents are as follows:(1) The researches of test cases in CTCS-3 and mutation testing at home and abroad are analyzed. At the same time, the mutation testing technique and the timed automata theory are also introduced in detail, which support the further research.(2) The mutation testing technique and the timed automata theory are combined. On this basis, the mutation testing method in CTCS based on TA is proposed, which includes three parts:the realization of formal modeling in CTCS-3, the mutation analysis in timed automata and evaluation of test case set, and the improvement of test case set based on the analysis of the mutated models. Thus a closed loop of the complete study system is built.(3) The mutation testing method based on timed automata is applied to the level transition scenario and RBC handover scenario, which are two typical scenarios in CTCS-3. Firstly, the formal models of the scenarios are built and the conformance relation between models and specifications is verified. Secondly, the mutation analysis and evaluation of test case set’s completeness focused on models are executed to get the evaluation index. Finally, the test case set is revised and supplemented based on the analysis process of the mutated models, by which the completeness of the original test case set is improved.(4) Using C# as the development language under Visual Studio2010 design platform, the assistant tool for mutant generation is realized. In the mutation analysis process, the tool can generate mutants semi-automatically according to the constraint of mutation operators, which provides convenient conditions for mutant generation.