A test sequence generation method of zone controller based on timed automata

SONG Shuang1, CHEN Yue-dong2

（1. Huizhou Engineering Vocational College, Huizhou 516000, China；2. Shenzhen Evsystem New Energy Technology Co., Ltd, Shenzhen 518118, China）

Abstract： In order to solve the problem of artificial generation and low efficiency of test sequences for zone controller (ZC), a model-based automatic generation method of test sequence is proposed. Firstly, the timed automata model is established based on function analysis of the zone controller, and the correctness of the model is verified by UPPAAL. Then by parsing the timed automata model files, state information and transition conditions can be extracted to generate test case sets. Finally, according to the serialization conditions of test cases, the test cases are serialized into test sequences by using the improved depth first search algorithm. A case, the ZC controls the train running within its jurisdiction, shows that the method is correct and can effectively improve the efficiency of test sequence generation.

Key words： test sequence; zone controller (ZC); timed automata model; file parsing; case serialization

CLD number： TP273  Document code： A

Article ID： 1674-8042（2019）03-0266-11  doi： 103969/jissn1674-8042201903010

References

［1］Yuan L, Lv J D, Liu Y, et al. Research on model-based test case generation method of onboard subsystem in CTCS-3. Journal of the China Railway Society, 2014, 36(8): 55-62.
［2］Wang Q Q, Zhang Y. Application of UML in the generation of CTCS-3 test cases. Urban Mass Transit, 2012, 15(3): 41-44.
［3］Lv J D, Zhu X L, Li K C, et al. Model-based test case automatic generation of CTCS-3 train control system. Journal of Southwest Jiaotong University, 2015, 50(5): 917-927.
［4］Zhao W H, Lv J D, Yuan L, et al. On scenario-based automatic test cases generation method for onboard devices. Computer Applications and Software, 2015, 32(3): 65-68.
［5］Qaisar A M, Johan L, Linas L. Scenario-based test case generation using Event-B models. In: Proceedings of 2009 First International Conference on Advances in System Testing and Validation Lifecycle, Portugal, 2009: 31-37.
［6］Xie L, Yang Y. Model-based automatic generation of test case of route establishment process. Railway Standard Design, 2017, 61(2): 109-116.
［7］Chen W. Data research and design for zone controller in urban railway transit. Chengdu: Southwest Jiaotong University, 2015: 19-32.
［8］Kang R W. The research on modeling methods and verification of Chinese train control system level 3 based on timed automata. Beijing: Beijing Jiaotong University, 2013: 15-27.
［9］Xi L, Zhou Q L. UPPAAL-based real-time testing: new coverage criteria and length-optimal test generation. In: Proceedings of Information Theory and Information, Beijing, 2010: 117-120.
［10］He H H. Formal modeling and verification of CBTC zone controller based on time automation. Lanzhou: Lanzhou Jiaotong University, 2015: 14-30.
［11］Mu J C, Xin W, Ma L C, et al. Verification method for completeness of CTCS-3 test case based on cause-effect graph. China Railway Science, 2016, 37(1): 124-131.
［12］Jong G H, Jong H B, Hyun J J, et al. Applicability test on black-box testing tool of railway signaling system in consideration of the convenience of use. In: Proceedings of International Conference on Control, Seoul, 2014: 1489-1495.
［13］Chen X, Jiang P, Zhang Y F, et al. Method of automatic test case generation for safety-critical scenarios in train control systems. Journal of Software, 2015, 26(2): 269-278.
［14］Liu X J, Du H Q, Zhu Z L. Approach to generation and construction of test-cases based on timed automata. Micrielectronics & Computer, 2015, 32(9): 169-176.
［15］Valentin C,Franz W.Using dependency relations to improve test case generation from UML statecharts. In: Proceedings of the 37th Annual Computer Software and Applications Conference Workshops, Japan, 2013: 71-76.

基于时间自动机模型的区域控制器测试序列自动生成方法

宋爽1， 陈跃东2

（1. 惠州工程职业学院， 广东 惠州 516000；2. 深圳熙斯特新能源技术有限公司， 广东 深圳 518118）

摘要:针对目前区域控制器测试序列人工生成， 测试效率低的问题， 提出了一种基于模型的测试序列自动生成方法。 首先， 对区域控制器的功能进行分析， 基于时间自动机理论建立区域控制器的时间自动机模型， 并利用UPPAAL对模型的正确性进行验证分析； 然后， 解析时间自动机模型文件， 提取状态信息和变迁条件， 生成测试案例集； 最后， 根据测试案例的串接条件， 利用改进的深度优先搜索算法将测试案例串接成测试序列。 对比区域控制器控制列车在其管辖范围内正常运行功能人工生成的测试序列和自动生成的测试序列， 结果证明， 该测试序列生成方法可行， 且能够有效提高测试序列生成效率。

 
关键词:测试序列； 区域控制器； 时间自动机模型； 文件解析； 案例串接

引用格式：SONG Shuang, CHEN Yue-dong. A test sequence generation method of zone controller based on timed automata. Journal of Measurement Science and Instrumentation, 2019, 10（3）： 266-276. ［doi： 103969／jissn1674-8042201903010］

[full text view]