多端口形式化测试自动生成方法在CTCS-3车载系统中的应用  

Multi-port Based Automatic Formal Testing Generation and Its Application in CTCS-3 Level On-board System

作　　者：赵显琼[1] 唐涛[1] 

机构地区：[1]北京交通大学轨道交通控制与安全国家重点实验室

出　　处：《铁道学报》2011年第7期44-51,共8页Journal of the China Railway Society

基　　金：国家自然科学基金项目(60634010);国家高技术研究发展计划(863计划)(2009AA11Z221);轨道交通控制与安全国家重点实验室自主研究课题(RCS2008ZZ005)

摘　　要：针对CTCS-3列控系统测试中普遍存在的需要多个端口协同测试的问题,在时间输入输出自动机(TIOA)的基础上,提出端口标记的时间输入输出自动机(LpTIOA)。LpTIOA除在模型中能够反映系统的时间约束特性外,还能反映系统输入输出行为对应的端口信息,利用这些信息对基于覆盖度的搜索算法进行相应改进,形成包含端口信息的测试自动生成算法,用于生成满足给定覆盖度标准的测试套。文中还描述了运用UP-PAAL工具对LpTIOA模型实现建模的方法,并运用COVER工具实现对经过UPPAAL验证的CTCS-3级车载系统LpTIOA模型的测试套自动生成。For the purpose of solving the problem of multi-ports testing of the real-time system such as the CTCS-3 level On-Borad subsystem,this paper presents the Labled-ports Timed Input/Output automata（LpTIOA） based on the Timed Input/Output automata（TIOA）.The LpTIOA model can describe the time constraining information and ports information of the system behaviors.Making use of these information,this paper improves the reachability algorithm and forms the new testing generation algorithm including the ports information to generate the test suites according to different given coverage criterias.This paper also depicts the LpTIOA modelling method with the use of the UPPAAL tool and applies the COVER tool to generate automatically the test suites of the CTCS-3 Level On-borad Subsystem LpTIOA model though UPPAAL verification.

关 键 词：CTCS 时间自动机 车载系统 UPPAAL 实时系统 COVER 

分 类 号：TP301.1[自动化与计算机技术—计算机系统结构] U284.48[自动化与计算机技术—计算机科学与技术]