CAJ | 학술논문

本文提出一种基于变异模型的CTCS-3级列控系统测试用例自动生成方法。根据列控系统需求规范，建立它的SMV（Symbolic Model Verifier）模型，对此模型进行变异，将变异之后的模型输入到模型检验器SMV中，利用模型检验生成反例的技术，自动生成测试用例，提高了测试用例的生成效率。并以CTCS-3级列控系统的无线闭塞中心（RBC）切换场景为例，验证了该方法的有效性。
본문제출일충기우변이모형적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 speciifcation 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 efifciency 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, veriifed the effectiveness of the method.