基于模型的CTCS-3级列控系统测试案例自动生成方法

吕继东; 朱晓琳; 李开成; 唐涛; 王海峰

doi:10.3969/j.issn.0258-2724.2015.05.023

基于模型的CTCS-3级列控系统测试案例自动生成方法

doi: 10.3969/j.issn.0258-2724.2015.05.023

基金项目:

国家973计划项目(2014CB340700)

国家自然科学基金资助项目(61304185)

中央高校基本科研业务费专项资金资助项目(2014JBM022)

详细信息

作者简介:
吕继东(1981-),男,讲师,博士,研究方向为混杂系统建模及其应用、高速铁路列控系统关键技术,E-mail:jdlv@bjtu.edu.cn

计量
- 文章访问数: 795
- HTML全文浏览量: 95
- PDF下载量: 398
- 被引次数: 0
出版历程
- 收稿日期: 2014-03-03
- 刊出日期: 2015-10-25

Model-Based Test Case Automatic Generation of CTCS-3 Train Control System

摘要

摘要: 为了提高CTCS-3级列控系统测试案例生成效率,提出了基于混合通信顺序进程(hybrid communication sequential process, HCSP)形式化模型和时间自动机(timed automaton, TA)形式化模型的列控系统测试案例自动生成方法;建立了列控系统运营场景的时序模型,分析了列控系统运营场景规范中时序功能的正确性;在时序模型的基础上,设计了满足全状态、全变迁和自定义-使用3种领域无关覆盖准则的列控系统测试案例自动生成算法,并以RBC(radio block center, RBC)切换场景为例,生成了100%全状态、全变迁和自定义-使用覆盖准则的测试案例套.从测试套数量、测试时间和内存消耗3个方面分析测试案例的生成效率表明:自定义-使用覆盖准则的测试案例套测试时间和内存消耗最小,分别为0.02 s和9.4 MB,本文方法提高列控系统测试案例生成效率最大达30%.
- 形式化模型 /
- 列控系统 /
- HCSP /
- TA /
- 测试案例自动生成 /
- 测试套
Abstract: In order to improve the test case generation efficiency of the CTCS-3 train control system, a test case automatic generation method is proposed based on formal models of hybrid communication sequential process (HCSP) and timed automata. Then, timing models for operation scenarios in the train control system are built to verify its real-time function. Based on the timing models, test case automatic generation algorithms are designed for three domain independent coverage criteria, including all location, all edge and definition-use pair in the train control system. Taking the typical radio block center (RBC) handover scenario as an example, 100% function coverage test suites with all-location, all-edge and definition-use pair test coverage criteria are automatically derived. In addition, the efficiency of the test case generation method is analyzed from the aspects of test suite number, time consumption, and memory cost. The results show that among the three 100% function coverage test suites, the user-defined pair test criterion consumes a minimum time of 0.2 s and a minimum memory of 9.4 blocks, and the proposed method can enhance the test case generation efficiency by a maximum of 30% in the train control system.
- formal model /
- train control system /
- HCSP /
- timed automata /
- test case automatic generation /
- test suites

HTML全文

参考文献(37)

吕继东. 列车运行控制系统分层形式化建模与验证分析

[D]. 北京:北京交通大学,2011.

古天龙. 软件开发的形式化方法

CHAOCHEN Z, HANSEN M. Duration calculus a formal approach to real-time systems

DONG Jinsong, HAO Ping, QIN Shengchao, et al. Timed automata patterns

[M]. 北京:高等教育出版社,2005: 6-8.

HOARE C A R. Communicating sequential processes

LIU Jiang, L Jidong, ZHAO Quan. Programming languages and systems: a calculus for hybrid CSP

[M]. : Springer-Verlag, 2003: 14-16.

BEIZER B. Black-box testing, techniques for functional testing of software and systems

张勇,王超琦. CTCS-3级列控系统车载设备测试序列优化生成方法

[J]. IEEE Transactions on Software Engineering, 34, 2008: 844-845.

徐中伟,吴芳美. 形式化故障树分析建模和软件安全性测试

[J]. Communications of the ACM, 1978, 21(8): 666-677.

赵显琼,唐涛. 多端口形式化测试自动生成方法在CTCS-3车载系统中的应用

张曙光. CTCS-3级列控系统总体技术方案

ALUR R, DILL D L. A theory of timed automata

[M]. Berlin: Springer, 2010: 1-15.

吕继东,唐涛. 高速铁路列控系统运营场景实时性建模与验证

[M]. New York: Wiley, 1995: 39-41.

ZHOU Chaochen, WANG Ji, ANDERS P. Ravn a formal description of hybrid systems

BEHRMANN G, LARSEN K G, MOLLER O, et al. UPPAAL-present and future

HESSEL A, PETTERSSON P. CoVer: a real-time test case generation tool

[J]. 中国铁道科学,2011,32(3): 100-106. ZHANG Yong, WANG Chaoqi. The method for the optimal generation of test sequence for CTCS-3 on-board equipment

[J]. China Railway Science, 2011, 32(3): 100-106.

[J]. 同济大学学报:自然科学版,2001,29(11): 1299-1302. XU Zhongwei, WU Fangmei. Formal fault tree analysis modeling and software safety testing

[J]. Journal of Tongji University: Natural Science, 2001, 29(11): 1299-1302.

[J]. 铁道学报,2011,33(7): 44-51. ZHAO Xianqiong, TANG Tao. Multi-port based automatic formal testing generation and its application in CTCS-3 level on-board system

[J]. Journal of the China Railway Society, 2011, 33(7): 44-51.

[M]. 北京.中国铁道出版社,2008: 49-50.

[J]. Theoretical Computer Science, 1994, 126: 183-235.

[J]. 铁道学报,2011,33(6): 54-61. L Jidong, TANG Tao. Modeling and verification of time constraints of operation scenarios of high-speed train control system

[J]. Journal of the China Railway Society, 2011, 33(6): 54-61.

[C]//Proc. of the DIMACS/SYCON Workshop on Hybrid Systems III: Verification and Control. New York: Springer-Verlag,1996: 511-530.

[C]//Proc. of the 40th IEEE Conference on Decision and Control. Orlando:

[s. n.], 2001: 2881-2886.

[C]//19th IFIP International Conference on Testing of Communicating Systems and 7th International Workshop on Formal Approaches to Testing of Software. Berlin: Springer, 2007: 73-77.

施引文献

附加材料(0)

访问统计

点击查看大图

计量

文章访问数: 795
HTML全文浏览量: 95
PDF下载量: 398
被引次数: 0

基于模型的CTCS-3级列控系统测试案例自动生成方法

doi: 10.3969/j.issn.0258-2724.2015.05.023

作者简介: 吕继东(1981-),男,讲师,博士,研究方向为混杂系统建模及其应用、高速铁路列控系统关键技术,E-mail:jdlv@bjtu.edu.cn

计量

出版历程

Model-Based Test Case Automatic Generation of CTCS-3 Train Control System

计量

出版历程

目录

作者简介:
吕继东(1981-),男,讲师,博士,研究方向为混杂系统建模及其应用、高速铁路列控系统关键技术,E-mail:jdlv@bjtu.edu.cn