基于变异模型的CTCS-3级列控系统测试用例自动生成方法研究  

Mutation model-based generation of test cases for CTCS-3 Train Control System

作　　者：刘晓亮[1] 袁磊[1] 吕继东[2] 魏国栋[2] 富德佶 

机构地区：[1]北京交通大学轨道交通控制与安全国家重点实验室,北京100044 [2]北京交通大学轨道交通运行控制系统国家工程研究中心,北京100044

出　　处：《铁路计算机应用》2015年第6期54-57,60,共5页Railway Computer Application

基　　金：北京高等学校青年英才计划项目(YETP0580);中央高校基本科研业务费专项资金资助(2014JBM022);国家自然科学基金资助项目(61304185)

摘　　要：本文提出一种基于变异模型的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.

关 键 词：变异模型 列控系统 测试用例 模型检验 SMV 

分 类 号：U284.482[交通运输工程—交通信息工程及控制] TP39[交通运输工程—道路与铁道工程]