基于约束求解的城市轨道交通CBTC系统事件序列测试用例生成方法  

An event sequence test generation approach for urban rail transit CBTC system based on constraint solving

作　　者：覃瑶 张亚东[1] 饶畅 段峰 郭进[1] QIN Yao;ZHANG Yadong;RAO Chang;DUAN Feng;GUO Jin(School of Information Science and Technology,Southwest Jiaotong University,Chengdu 611756,China;College of Traffic and Transportation,Chongqing Jiaotong University,Chongqing 400074,China;School of Software&IoT Engineering,Jiangxi University of Finance and Economics,Nanchang 330013,China)

机构地区：[1]西南交通大学信息科学与技术学院,四川成都611756 [2]重庆交通大学交通运输学院,重庆400074 [3]江西财经大学软件与物联网工程学院,江西南昌330013

出　　处：《铁道科学与工程学报》2023年第9期3525-3535,共11页Journal of Railway Science and Engineering

基　　金：四川省科技计划资助项目(2021YJ0070);中央高校基本科研业务费专项资金资助项目(2682022ZTPY084);中国铁路总公司科技研究开发计划课题(N2018G062,K2018G011);重庆交通大学科技研究计划(XJ2021003201);重庆市教委科技项目(KJQN202300750)。

摘　　要：城市轨道交通CBTC系统采用无线通信技术实现车−地连续双向、大容量信息传输。当前,我国正在大力发展自主化CBTC系统,为保障系统软件安全性,对系统进行信息交互测试是极为必要的。针对现有研究对CBTC系统的信息交互顺序测试不充分而引发的系统软件安全性问题,提出一种基于约束求解的事件序列测试用例生成方法。首先,根据系统蕴含的信息交互事件及其约束关系,提出一种基于事件索引的约束处理方法,实现顺序约束条件的1阶逻辑表示,继而采用约束求解器实现测试用例生成过程中的合法性校验及可扩展性校验。然后,基于贪心算法框架,提出事件序列测试用例的初始化、扩展与校验策略,实现事件序列测试用例集的高效精简生成。最后,以列车进站场景下的CBTC系统移动授权生成功能为研究对象,辨识各子系统间的信息交互事件、交互顺序及其约束,采用所提方法构建CBTC系统事件序列测试用例集。结果表明,所提方法可高效精简生成满足约束条件与覆盖准则的事件序列测试用例集,提高了测试的有效性与完备性。与穷举法相比,所提方法的测试用例集规模精简幅度可达到72.5%。与随机法相比,在生成相同规模的测试用例集时,所提方法的t-维事件序列覆盖率显著高于随机法,可在保证事件序列检错效力的前提下提高测试效率,从而为高效开展CBTC系统的信息交互顺序测试提供了理论依据。The urban rail transit CBTC system adopts wireless communication technology to realize continuous two-way,high-capacity information transmission between train and ground.In recent years,developing CBTC system with independent intellectual property rights is strongly encouraged and adopted by society.To preserve system safety,conducting information interaction testing on software becomes extremely necessary.Aiming at solving the safety issue of CBTC software caused by insufficient information interaction testing,this paper proposed an event sequence test generation approach based on constraint solving strategy.First,according to the interaction events and their constraints subsumed in the system,a constraint handling method was proposed based on event indices such that constraints are presented in first-order logic instead of sequential constraints.A constraint solver was further introduced for validity check and extensibility check during test generation.Next,based on a greedy algorithm framework,the strategies of test initialization,expansion and verification were proposed for generating tests more efficiently and effectively.Finally,taking as case study the Movement Authority Generation function of CBTC system under scenario of train entering station,information interaction events and constraints were identified and modeled.And the event sequence tests were generated.Results show that the proposed approach can generate tests in a more efficient way that satisfy constraints and coverage criteria,which enhances the effectiveness and completeness of testing.When compared to the exhaustive approach,the scale of the generated tests can be reduced by 72.5%.When compared to the random approach under the same size of test set,the t-way coverage of the proposed approach reaches significantly higher,which rises the test efficiency while preserving a strong ability for fault detection.Thus,a strong theory basis is provided for conducting efficient information sequence testing on CBTC system.

关 键 词：CBTC系统 事件序列测试 测试用例生成 SMT求解器 

分 类 号：U284.48[交通运输工程—交通信息工程及控制]