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

刘晓亮; 袁磊; 吕继东; 魏国栋; 富德佶

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

1.
北京交通大学轨道交通控制与安全国家重点实验室,北京 100044;
2.
北京交通大学轨道交通运行控制系统国家工程研究中心,北京 100044

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

详细信息

作者简介:
刘晓亮,在读硕士研究生;袁磊,讲师。

中图分类号: U284.482:TP39
计量
- 文章访问数: 100
- HTML全文浏览量: 0
- PDF下载量: 87
出版历程
- 收稿日期: 2014-11-12
- 刊出日期: 2015-06-24

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

1.
State Key Laboratory of Rail Traffic Control and Safety, Beijing Jiaotong University, Beijing 100044, China;
2.
National Engineering Research Center of Train Control System, Beijing Jiaotong University, Beijing 100044, China

摘要

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

HTML全文

参考文献(15)

[1]	唐涛．列车运行控制系统[M]．北京：中国铁道出版社,2012．
[2]	袁磊,吕继东,刘雨,等．一种全覆盖的列控车载系统测试用例自动生成算法研究[J]．铁道学报,2014,36（8）：55-62．
[3]	刘新忠,徐高潮,胡亮,等．一种基于约束的变异测试数据生成方法 [J]．计算机研究与发展,2011,48（4）：617-626．
[4]	金丹．安全计算机平台测试序列的生成及应用[D]．北京：北京交通大学,2013．
[5]	陆毅明．面向对象程序的变异测试方法研究—基于代数式规格的变异测试系统的研究与实现[D]．上海：上海交通大学,2007.
[6]	Hamlet R G. Testing programs with the aid of a compiler[J].IEEE Transactions on Software Engineering, 1977, 3(4): 279-290．
[7]	单锦辉,高友峰,等．一种新的变异测试数据自动生成方法 [J].计算机学报,2008,31（6）：1025-1034．
[8]	Ammann P E, Black P E, Majurski W. Using model checking to generate tests from specifications[C]. Formal Engineering Methods,1998. Proceedings. Second International Conference on. IEEE, 1998: 46-54．
[9]	郭文章．ATS系统内部通信协议的设计及形式化验证[D].北京：北京交通大学,2009.
[10]	张岩．列车运行控制系统软件故障相关形式化测试方法[D]．北京：北京交通大学,2012.
[11]	Ammann P, Ding W, Xu D. Using a model checker to test safety properties[C]. Engineering of Complex Computer Syst-ems, 2001. Proceedings. Seventh IEEE International Confe-rence on. IEEE, 2001: 212-221．
[12]	Black P E, Okun V, Yesha Y. Mutation of model checker specifications for test generation and evaluation[M]. New York. Springer US, 2001: 14-20．
[13]	Okun V. Specification mutation for test generation and analysis[D]．University of Maryland Baltimore County, 2004.
[14]	中华人民共和国铁道部．CTCS-3s级列控系统系统需求规范（SRS）[S]．北京：中国铁道出版社, 2009．
[15]	吕继东,唐涛．高速铁路列控系统运营场景实时性的建模与验证[J] .铁道学报,2011,33（6）：54-61.

施引文献

资源附件(0)

计量

文章访问数: 100
HTML全文浏览量: 0
PDF下载量: 87
被引次数: 0

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

作者简介: 刘晓亮,在读硕士研究生;袁磊,讲师。

计量

出版历程

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

计量

出版历程

目录

作者简介:
刘晓亮,在读硕士研究生;袁磊,讲师。