中文摘要：

本文提出一种基于变异模型的CTCS-3级列控系统测试用例自动生成方法。根据列控系统需求规范,建立它的SMV（Symbolic Model Verifier）模型,对此模型进行变异,将变异之后的模型输入到模型检验器SMV中,利用模型检验生成反例的技术,自动生成测试用例,提高了测试用例的生成效率。并以CTCS-3级列控系统的无线闭塞中心（RBC）切换场景为例,验证了该方法的有效性。

英文摘要：

Based on mutation model of CTCS-3 Train Control System, this paper proposed a mutation model-based method to generate test cases automatically. According to the requirements specification of Train Control System, the SMV model was established and mutated. The mutated model was put into the SMV model checker. The test case was generated automatically by using the model checking methods and the efficiency of the test case generation was improved dramatically. Finally, a scenario of Radio Block Center（RBC） handover in CTCS-3 Train Control System was taken as an example, verified the effectiveness of the method.