Mutation Timed Automata with Input and Output-Based Method of Generating Test Suites for Chinese Train Control System Level 3
-
摘要: 为了研究高覆盖已知故障集的中国列车运行控制系统三级(CTCS-3)测试案例生成方法,提出了一种基于输入输出时间自动机(TAIO)变异分析的测试案例生成方法. 结合列控系统模式转换的故障特点,设计了包含模式转换已知故障的8种变异算子(改变行为、改变目标位置、改变源位置等),形成了15 106个变异体;利用输入输出一致性关系(tioco)和k-Bounded模型检验方法生成了10 843个测试案例;应用一致性关系分数(CRS)、平均一致性关系分数(ACRS)和加权一致性关系分数(WCRS)进行了故障覆盖度的分析. 研究结果表明:该方法设计和生成的测试案例能够有效覆盖改变行为、改变不变量和增加sink位置3种故障模式,而对于约束取反和复位取反的故障模式覆盖度不高,需通过额外的观测信息来检测故障.
-
关键词:
- CTCS-3级列控系统 /
- 输入输出时间自动机(TAIO) /
- 变异分析 /
- 模式转换 /
- 测试案例
Abstract: In order to design and select the proper set of test cases so that all the known faults can be covered, an automatic test suite generation method was proposed for the Chinese train control system level 3 (CTCS-3) based on timed automata with input and output (TAIO) and mutation analysis. Firstly, according to the characteristics of the fault modes of the system mode transition, kinds of mutation operators (change action, change target, change source, etc.) had been designed, and 15106 mutants were generated. Secondly, based on the timed input and output conformance relation (tioco) and the k-Bounded model checking technique, 10 843 test cases were generated. Finally, the conformance relation score (CRS), average conformance relation score (ACRS) and weighted conformance relation score (WCRS) had been introduced to analyze the coverage of faults domain. The results show that the test cases generated can effectively cover the fault modes of change action, change invariant and sink location, however, the negate guard and invert reset fault modes cannot be effectively covered, which may require additional information of observation for the fault detection. -
表 1 CTCS-3级列控系统模式转换
Table 1. Mode conversion of CTCS-3 train control system
模式 模式转换 SB SB->SH,SB->FS、SB->OS,SB->CO,
SB->SL,SB->TR,SB->ISSH SH->SB,SH->TR,SH->IS FS FS->SB,FS->SH,FS->OS,FS->CO,FS->TR,FS->IS OS OS->SB,OS->SH,OS->FS,
OS->CO,OS->TR,OS->ISCO CO->SB,CO->SH,CO->FS,
CO->OS,CO->TR,CO->ISSL SL->SB,SL->IS TR TR->PT,TR->IS PT PT->SB,PT->SH,PT->FS,
PT->OS,PT->CO,PT->ISIS IS->SB 表 2 车载设备与外部环境的交互
Table 2. Interaction between onboard and ground
设置对象 交互对象 具体交互 ActionInfor_D2O Driver<->
On-boardIsolate,TurnOn,TurnOff,ComfirmRashTrip,RequestSH,PromptCO,Override,ComfirmInfo,SendSleep,ChooseNotSH,RecoverBrake,PowerOn ActionInfor_R2O RBC<->On-board SendMSS,PermitSH,SendCOMA,UnconStop,ComBrakeInfo ActionInfor_B2O Train<->On-board Stop,LoseSleep,Store,NotOverride,MaxIntoCO,MinIntoEOA,RashTrip,StopInOS,StopInSH,COMode ActionInfor_T2O Balise<->On-board NotSpecMode,NotInOS,NotInSH,NotLink,NotVersion 表 3 TAIO A变异体模型和测试案例生成时间和内存消耗统计
Table 3. Statistics of TAIO A execution time and memory consumption for mutants and test suites
序号 变异算子 变异体模型/个 生成时间/s 内存消耗/MB 测试案例/个 生成时间/s 内存消耗/MB 1 改变行为(CA) 1388 1.95 26.88 1388 36.42 3.16 2 改变目标位置(CT) 6549 9.92 153.00 6050 184.51 13.24 3 改变源位置(CS) 6549 9.68 153.00 3243 129.33 7.18 4 改变约束(CG) 52 0.15 1.21 20 2.55 0.04 5 约束取反(NG) 111 0.22 2.74 10 4.11 0.02 6 改变不变量(CI) 13 0.07 0.31 13 1.28 0.02 7 增加sink位置(SL) 111 0.28 2.89 111 4.51 2.07 8 复位取反(IR) 333 0.56 8.15 8 11.06 0.02 9 总计 15106 22.83 348.18 10843 373.77 25.75 表 4 测试案例生成方法分析比较统计
Table 4. Statistics of TAIO mutation-based test suite generation and the others
测试案例生
成方法测试案
例/个生成时
间/s消耗内
存/MB完备性 基于TAIO变异分析 10843 373.77 25.75 较好 基于时间自动机模型 7982 486.52 5688.04 一般 基于随机测试 5602 4296.63 1029.22 一般 基于等价类划分 12803 6750.00 864.88 较好 表 5 模式转换测试案例一致性关系分数
Table 5. Conformance relation score of test suites
项目 一致性关系
分数平均一致性
关系分数加权一致性
关系分数改变行为 1.00 0.72 0.80 改变目标位置 0.92 改变源位置 0.50 改变约束 0.38 约束取反 0.09 改变不变量 1.00 增加sink位置 1.00 复位取反 0.03 -
唐涛. 列车运行控制系统[M]. 北京: 中国铁道出版社, 2012: 234-251. 袁磊,吕继东,刘雨,等. 一种全覆盖的列控车载系统测试案例自动生成算法研究[J]. 铁道学报,2014,36(8): 55-62. doi: 10.3969/j.issn.1001-8360.2014.08.010YUAN Lei, LÜ Jidong, LIU Yu, et al. Reserach on model-based test case generation method of onboard subsystem in CTCS-3[J]. Journal of the China Railway Society, 2014, 36(8): 55-62. doi: 10.3969/j.issn.1001-8360.2014.08.010 BEIZER B. Black-box testing: techniques for functional testing of software and systems[M]. New York: John Wiley & Sons, Inc. ,1995: 1192-1 198. KRICHEN M, TRIPAKIS S. Black-box conformance testing for real-time systems[M]. [S.l.]: Springer, 2004: 4-10. 吕继东,朱晓琳,李开成,等. 基于模型的CTCS-3级列控系统测试案例自动生成方法[J]. 西南交通大学学报,2015,50(5): 917-927. doi: 10.3969/j.issn.0258-2724.2015.05.023LÜ Jidong, ZHU Xiaolin, LI Kaicheng, et al. Model-based test case automatic generation of CTCS-3 train control system[J]. Journal of SouthWest Jiaotong University, 2015, 50(5): 917-927. doi: 10.3969/j.issn.0258-2724.2015.05.023 梁茨,郑伟,李开成,等. 基于路径优化算法的测试序列自动生成及验证[J]. 铁道学报,2013,35(6): 53-58. doi: 10.3969/j.issn.1001-8360.2013.06.009LIANG Ci, ZHENG Wei, LI Kaicheng, et al. Automated generation of test case and sequences based on path optimization algorithm[J]. Journal of the China Railway Society, 2013, 35(6): 53-58. doi: 10.3969/j.issn.1001-8360.2013.06.009 陈鑫,姜鹏,张一帆,等. 一种面向列车控制系统中安全攸关场景的测试案例自动生成方法[J]. 软件学报,2015,26(2): 269-278.CHEN Xin, JIANG Peng, ZHANG Yifang, et al. Method of automatic test case generation for safety-critical scenarios in train control systems[J]. Journal of Software, 2015, 26(2): 269-278. TRETMANS J. Model based testing with labelled transition systems[C]//Formal Methods and Testing. [S.l.]: Springer, 2008: 1-38. AICHEMIG B K, LORBER F, NICKOVIC D. Time for mutants: model-based mutation testing with timed automata[M]. [S.l.]: Springer, 2013: 23-26. BERTRAND N, JERON T, STAMER A, et al. Off-line test selection with test purposes for non-deterministic timed automata[J]. Tools and Algorithms for the Construction and Analysis of Systems, 2011: 392-402. ABOUTRAB M S, COUNSELL S, HIERONS R M. Specification mutation analysis for validating timed testing approaches based on timed automata[C]//Computer Software and Applications Conference. [S.l.]: IEEE, 2012: 660-669. BAHAREH B, MARTIN L. Exact incremental analysis of timed automata with an SMT-solver[C]//Formal Modeling & Analysis of Timed Systems-international Conference. [S.l.]: Springer, 2011: 177-192. JIA Y, HARMAN M. An analysis and survey of the development of mutation testing[J]. IEEE Transactions on Software Engineering, 2011, 37(5): 649-678. doi: 10.1109/TSE.2010.62 KRICHEN M, TRIPAKIS S. Conformance testing for real-time systems[M]. [S.l.]: Kluwer Academic Publishers, 2009: 238-304. 铁道部科技司. CTCS-3级列控系统标准规范-CTCS-3级列控系统系统需求规范(SRS)(第一册)[M]. 北京: 中国铁道出版社, 2009: 5-10. 徐伟,王林章,李宣东. 基于分类树的随机测试用例生成[J]. 计算机科学,2009,36(1): 263-266. doi: 10.3969/j.issn.1002-137X.2009.01.067XU Wei, WANG Linzhang, LI Xuandong. Classification tree-based random test case generation[J]. Computer Science, 2009, 36(1): 263-266. doi: 10.3969/j.issn.1002-137X.2009.01.067 HUANG W L, PELESKA J. Complete model-based equivalence class testing[J]. International Journal on Software Tools for Technology Transfer, 2014, 18(3): 1-19.