基于有色petri网的车载设备模式转换测试序列生成方法-赵晓宇.pdf

《基于有色petri网的车载设备模式转换测试序列生成方法-赵晓宇.pdf》由会员分享，可在线阅读，更多相关《基于有色petri网的车载设备模式转换测试序列生成方法-赵晓宇.pdf（9页珍藏版）》请在淘文阁 - 分享文档赚钱的网站上搜索。

1、第3 8卷，第4期2 0 1 7年7月中 国 铁 道 科 学CHINA RAILWAY SCIENCEV0138 No4July，2017文章编号：10014632(2017)04011509基于有色Petri网的车载设备模式转换测试序列生成方法赵晓宇1，杨志杰2”，吕旌阳4(1中国铁道科学研究院研究生部，北京100081；2中国铁道科学研究院通信信号研究所，北京100081；3中国铁道科学研究院国家铁路智能运输系统工程技术研究中心，北京100081；4北京邮电大学信息与通信工程学院，北京100876)摘要：为高效、自动生成覆盖车载设备所有转换路径的测试序列，根据CTCS-3级列控系统系统需求

2、规范，首先基于有色Petri网构建车载设备模式转换(MTCPN)模型，并采用ASK-CTL公式和非标准状态空间查询法对MTCPN模型进行分析和验证，然后根据车载设备模式转换规则，将车载设备的工作模式及其转换路径映射为有向图，采用中国邮路算法求解有向图，生成1条最优邮路，并对该邮路进行二次优化，生成车载设备模式转换的测试目标序列集；将测试目标序列作为MTCPN模型的输入，仿真生成满足全路径覆盖准则的可执行的测试序列集和XML文件。验证结果表明：基于有色Petri网的测试序列生成方法能够满足测试需求，并且避免了既有方法的状态空间爆炸和搜索死循环问题，提高了测试效率。关键词：测试序列；车载设备；列车

3、控制系统；模式转换；有色Petri网；中国邮路算法；路径覆盖量中图分类号：U284482 文献标识码：A doi：103969jissn1001463220170416CTC孓3级列控系统由车载设备和地面设备组成，属于典型的安全苛求系统。为了验证其行为功能的正确性，并保证不同厂家设备的兼容性，对其系统的功能进行测试成为必不可少的环节。如何高效地自动生成覆盖车载设备所有转换路径的测试序列，是目前车载设备模式转换测试的关键性问题。现有测试方法以人工测试和现场测试为主，测试时间较长，测试费用昂贵，导致测试效率较低，并且在很多情况下已经无法满足测试的需求。在这种背景下，自动测试方法应运而生。针对车载设

4、备模式转换功能的测试序列生成问题，李伟1将其转化为中国邮路问题2，使用遗传算法生成测试序列；张勇3采用Edmonds-Johnson算法及LINGO工具解决测试序列生成问题；但文献1，3都未涉及具体的测试序列生成过程，仅给出了车载设备模式转换的测试顺序。测试序列的合理性验证方面，张仕雄4对CTCS-3级列控系统测试序列的合理性进行了验证，但仅对序列合理性进行了初步分析。近年来，基于模型的测试方法51有效地融合了形式化方法与传统测试技术，在形式化建模方法的基础上，自动生成大量可靠的测试用例，提高了人工编写测试用例的效率，缩短了与自动化程度较高的测试执行过程的距离。基于模型的列控系统测试方面，赵显

5、琼8针对多端口协同测试问题提出了端口标记的时间输人输出自动机(LpTIOA)；袁磊9提出了1种能够满足全状态、全变迁覆盖准则的测试套自动生成算法；并且文献89均通过UPPAAL和CoVer工具生成满足相应覆盖标准的测试套，但生成的测试套抽象层次太高，无法描述系统的并发行为；姜鹏10根据安全苛求攸关场景建模需求，扩充了UML的事件驱动机制和时间特性描述机制，并提出了1种面向安全攸关场景的测试用例自动生成方法，但UML无法描述系统的并发行为，不能进行模型检验，具有一定的局限性。相对于其他形式化语言，有色Petri网收稿日期：20160510；修订日期：20170412基金项目：中国铁路总公司科技研

6、究开发计划项目(2015X002一B)第一作者：赵晓宇(1990)，女，河南延津人，博士研究生。E-mail：zhaoxiaoyu059126com万方数据116 中国铁道科学 第38卷(CPN)nq3具有直观的图形表示和严密的数学基础，在描述系统的分叉、同步和并行等行为、层次化建模及处理数据方面具有很大优势；牟小玲14分析了目前基于Petri网的测试用例生成方法，并指出了未来研究方向。在CPN的建模方面，刘婧1阳针对BitTorrent协议的高并发性和交互行为复杂性，给出了协议的CPN层次模型，充分利用了CPN在层次建模、复杂数据处理与模型检验的优势。在CPN的模型检验方面，马国富16提出了

7、1种基于ASkCTL及模型检验理论的死标志合理性验证算法。在基于CPN的测试研究方面，Farooq17提出了基于控制流的测试序列生成方法，通过随机漫步算法对CPN模型的状态空间进行多次搜索，生成满足覆盖标准的测试例集合，但容易生成冗余的测试案例；刘婧18研究了基于CPN的输入输出一致性测试(IOCO)生成方法，并给出了1种基于CPN描述测试目的模型并驱动IOCO一致性测试选择的新方法”1；赵显琼20给出了基于CPN的测试案例自动生成算法和测试序列搜索算法；郑伟21对测试案例生成算法20进行了改进，提出了基于CPN的全路径覆盖优化算法和序列优选算法，后又提出了基于改进蚁群算法的测试序列生成方法2

8、 2|，用于提高自动测试执行的效率。总体而言，这些研究均采用启发式搜索算法生成测试用例，容易造成状态空间爆炸和死循环问题。同时，车载设备模式转换的复杂性，增加了传统搜索算法实现转换路径全覆盖的困难。相比而言，基于CPN的模拟仿真，属于状态空间的动态探索分析，是解决状态空间爆炸和死循环的有效途径。因此，本文基于CTCS-3级列控系统系统需求规范(SRS)23(简称规范)，针对车载设备模式转换的功能，提出基于CPN的车载设备模式转换测试序列生成方法。1基于CPN的车载设备模式转换测试序列生成方法11方法的总体框架基于CPN的车载设备模式转换测试序列生成方法的总体框架如图1所示，包括如下3个部分。(

9、1)根据规范，基于CPN构建车载设备模式转换(简称为MTCPN)模型，并采用ASK-CTL公式和非标准状态空间查询法对MTCPN模型进行分析与验证。(2)根据规范，采用中国邮路算法生成车载设备模式转换的测试目标序列。(3)将生成的测试目标序列作为MTCPN模型的输入，仿真生成满足全路径覆盖准则和CPN相应覆盖准则的可执行的测试序列集和XML文件集，避免了采用启发式搜索算法导致的状态空间爆炸和死循环问题。图1基于CPN的车载设备模式转换测试序列生成方法框架图12相关定义定义1：非层次化CPN模型采用9个元素表示，即CpN一(P，T，A，三，V，C，G，E，工)，其中各个元素的含义如下。(1)P为

10、库所的有限集合；T为变迁的有限集合；A为弧的有限集合；且满足Pn TPnATnA一乃，APTn丁P。(2)三为有限非空的颜色集合，用于定义模型中的数据类型；V为变量集合；且满足Type口E三，础V。(3)C(C：P一三)为着色函数，用于定义库所上允许的颜色类型，即从库所P到颜色集三的映射。(4)G(G：r+EXPR。)为守卫表达式函数，用于定义变迁上的守卫函数，给出了变迁的点火条件。(5)E(E：AEXPR。)为弧表达式函数，用于定义弧上的弧函数，满足而peE(口)一C(p)，即与弧连接的库所的着色函数约束着弧表达式的数据类型，其中Cm为集合C的多重集集合。(6)I(I：P-，EXPR垂)为初

11、始化赋值函数，万方数据第4期 基于有色Petri网的车载设备模式转换测试序列生成方法 117用于定义库所的初始数据赋值，满足TypeJ(夕)一C(P)Ms。定义2：CPN模块采用4个元素表示，即CPNM一(CPN，P。，Tsub，PT)，其中各个元素的含义如下。(1)C州为一个非层次化CPN模型。(2)P。P为端口位置集合；TsubT为替代变迁集合。(3)PT：PD。一IN，0UT，IO)为端口类型函数，用于定义端口位置；P。表示3种端口类型：输入端口IN)、输出端口(OUT)和输入输出端口IO)。定义3：层次化CPN模型采用4个元素表示，即CPNH一(S，SM，PS，FS)，其中各个元素的含

12、义如下。(1)S为CPN模块的有限集合，即S一(P，p，A5，驴，C，G，P，r)，E。b，Pk，P个)；其中，当S1，s2S，51S2时，有(P电UP)n(P5z U T2)一够。(2)SM：Ts曲一S为子模块函数，用于关联替代变迁和对应的CPN模块。(3)PS()P础()P潞幻(V tTsub)，用于定义端口间的关联性，P础()为替代变迁所在模块的端口库所，P裂。为与替代变迁对应的CPN模块的端口库所，满足V(p，P 7)Ps()，PT(p)=PT(p 7)，C(夕)一C(p)，j(户)，即具有关联性的库所是相通的。(4)FS2p是库所融合集，满足V(P，P7)，fsFS，C(P)一C(P

13、)，I(P)，即库所融合集中的所有库所是相通的。定义4：ASK_CTL状态公式表示如下，其中各参数的定义见文献24。A：一tt a IA A1 V A2 Il EU(A1，A2)l AU(A1，A2)一荭l a NOT(A)I A1 U A2 IIEU(Al，A2)J AU(Al，A2)定义5：ASK-CTL状态公式的语义如下，其中各参数的定义见文献24。(1)og，口ISttt总是为真；(2)og，口Ista，iif a在节点口上为真；(3)og，口ISt-I ANOT(A)，iif notog，口I=stA；，(4)og，u lStAl VA2一A1 UA2，iif og，可IStAl o

14、r og，口lstA2；(5)og，铆Is。，iifa一(s，(，6)，5 7)Ana IT，B；(6)og，勘IstEU(A：，Aj)，iifj丌vPaths(s)：了J：V0i勺：og，丌(口，) IStAl人V i巧：og，丌(剧i) IstA2；(7)og，剐I=s,AU(Ai，Ai)，iff了7rEvPaths(可)：J：Voi勺：og，7r(口i) l=-stAl八V i巧：og，丌(口i) IStA2。ASKCTL的变迁公式和语义也见文献24。2 MTCPN模型的构建和验证21 1wrCPN模型的构建根据规范可知：CTCS-3级列控车载设备有9种工作模式，即完全监控模式(FS)、

15、目视行车模式(OS)、引导模式(CO)、调车模式(SH)、隔离模式(IS)、待机模式(SB)、冒进防护模式(TR)、冒进后防护模式(PT)和休眠模式(SL)；且车载设备各工作模式之间存在的转换条件(即转换路径)数量见表1。表1车载设备的模式转换路径数量表不同模式之间的转换路径数量条FS oS 00 SL TR根据规范，提出以下8条建模规则。(1)采用分层(2层)建模规则构建MTCPN模型，上层模型只考虑各模式之间的转换路径，下层模型考虑各模式转换的具体转换流程。(2) 规范中的“转换条件18”是针对CTC孓2等级的，本文不做讨论。(3)为使MTCPN模型简洁且不失普遍性，除SH，IS和SL模式

16、外，默认其他模式均与RBC已建立通信会话，并且只考虑各模式转换流程，对模式转换后的流程不做处理。(4)为使MTCPN模型便于分析，凡是跟应答器相关的流程，均按照单个应答器处理。璐一1l111lO1O盯一oooooo，oo1O1O1OO1O1OOl1OO1O瓣=踮刚f2孑3豫盯盆万方数据118 中国铁道科学 第38卷(5)建模过程严格遵守车载设备模式转换规范，暂不考虑特殊情况。(6)MTCPN上层模型的模式转换均用替代变迁表示，具体的转换流程均在MTCPN下层模型表示。(7)MTCPN模型中，颜色的定义、变量和库所等的命名均遵循一定的规则，以辅助算法实现。(8)对数据内容的判断行为，均在守卫函数

17、中体现。由此构建出MTCPN模型。其中，上层模型如图2所示；下层模型共有39个，这里仅给出其中SB模式转FS模式的下层模型，如图3所示。图2 MTCPN模型的上层模型m矗nm fms93：a(!In le：val“Eq孓；阳九沁媳etl,5，0卜27in,ms93)ena图3 SB模式转FS模式的下层模型22 MTCPN模型的验证模型验证的基本思想是用状态迁移系统表示系统的行为，用模态时序逻辑公式描述系统的性质。Cheng等人将CPN与模型检验相结合，并在CPNTools工具中引人了1种扩展逻辑语言ASKCTLE2 4|。本节根据CPN模型检测理论，使用分支时序逻辑ASK-CTL公式及非标准状

18、态空间查询法对构建的MTCPN模型进行验证。万方数据第4期 基于有色Petri网的车载设备模式转换测试序列生成方法针对图2进行MTCPN模型的死锁分析，其结果如图4所示，可知MTCPN模型无死标识节点，属于强连通图，说明构建的MTCPN模型满足规范要求的模式转换功能。letvaI ridTextIOopenOut“DeadMarkings txt“val一；TextlO。output(fid，”List of dead markings：n”)val一霉EvalNodes0istD母adMafklngs()， fn n=INT。output(rid，nval一。Te媲Io，output(rid

19、，“、n Number of dead morkings：。val一黧INToutput(fid。egdl“$tDeadMarkings0)InTextIOctoseOut(fidend；图4 MTCPN模型的死锁分析结果针对图3进行转换规则的验证，其结果如图5所示。实际测试的车载流程中，车载设备的初始工作模式始终为SB模式，即库所SB的初始标记为1 7(6，true)(变量“6”表示MMODE=6，即车载模式为SB模式，变量“true”表示BWrieComm=true，即SB模式下车载设备已与无线闭塞中心RBC建立了通信连接，那么存在某条路径，使得SB模式可转人FS模式；同理，存在某条路径，

20、使得FS模式可转入TR模式，执行ASLCTL公式，返回执行结果“true”，如图5(a)所示；如果删除库所SB的初始标记，其返回vaI lsConsideredTs 1 fn：Arc o boolval myASKCTLformuta t MODAL fEXISTUNTIL(13囊F C”Is Dead Trans黼ON“,fn，j怠。trL。：b。Ifun IsConsideredTs a=(T1sBFsSBFs 1彗ArcToTl a)；vaI myASKCTLformulaMODAL(POS(AF(“Is Dead Transition“。IsConsideredTs)1evalnode

21、 myASKCT“ormula InitNode；fu九lsConsideredTs a=(T1FSTRReceiveMSGl6 1。矗rcToTl akcaI myASKCTLformulaMODAL(POS(AF(“Is Dead Transition“，lsConsidereb)jeval node myASKC飘ormula InitNode；￥al IsConsidered丁-fn：Arc-boo姻l m_I,ASKCTLformula m MODAL(EXI$LUNTIL m$Dead Transition”知)：Ava“t mtrue：bool(a)存在I作模式情况FvaI Is

22、ConslderedTs I fn：ArcbooIval myASKCTLformula I MODALEXIST_UNTIL(TT，AF(“Is Dead Transition“,fn：AvaIit。faIse：booIfun IsConsideredTs a-T1s8Fss矗lFs l瓣如cToTI a)；val myASKcTLformula班MODAL(POS(AF(“Is Dead Transition”，IsConsidere酣s)：oval_node myASKCTLformula Inode；n lseonsIde阳dTs a=(TI。弼丁RReceiveMi；G16 I*Ar

23、cTvl akamyASKCTLformulaMODAL(POS(AF(“Is Dead Transition”IsConsideredTs)iovalnode myASKCn如rmula InitNode；vaI lsConslderedTs z fn：Arc-booIvaI myASKCTLformula t MODAL fEXI玎_uNTIL(TT-F(Is Dead Transition”抽)：AvaI建-false：boo|(b)不存在工作模式情况F图5模式转换规则的验证结果结果如图5(b)所示，表示这种情况永远不会发生；如果设置库所FS的初始标记为1 7(o，true)，其执行结果

24、同样如图5(a)所示，说明构建的MTCPN模型符合车载设备模式转换流程。3测试目标序列集的生成方法对于传统的基于CPN模型的测试生成方法，大多数以空问搜索算法为基础，但这类方法容易陷入死循环，并且由于车载设备模式转换的复杂性，更加剧了模式转换测试序列实现转换路径全覆盖的困难。为了解决上述问题，针对规范采用中国邮路算法生成测试目标序列。根据车载设备模式转换规则，将车载设备的工作模式映射成有向图的顶点，车载设备的模式转换路径映射成有向图的弧，则可将表1转换成有向图D，如图6所示。图6车载设备模式转换有向图由图6和第22节可知，映射后的车载设备模式转换有向图为强连通图，即车载设备模式转换有向图存在最

25、优邮路，因此采用中国邮路算法生成测试目标序列，算法步骤如下。步骤1：针对有向图D中的所有顶点口iSB，SH，OS，CO，FS，TR，PT，IS，计算所有顶点让的人度与出度之差，即求解dD(饥)=dD(口：)一d古(可i) (其中d云(u：)为人度，矗去(功)为出度)。步骤2：如果所有顶点耽的d 7D(让)均为零，则原始有向图D为平衡欧拉图D 7，转入步骤5；否则转入步骤3。步骤3：利用Floyd算法求解各个顶点(可：，可，)间的最短距离矩阵F与最短路径矩阵P7。步骤4：针对各个不平衡点(即d7D(q)不为零的顶点)，根据改进Hungary算法求解此顶点的最优匹配方案，并为各个配对的不平衡点添加

26、最万方数据120 中国铁道科学 第38卷短路径，构造平衡欧拉图D 7。步骤5：对平衡欧拉图D7进行欧拉寻址，得到最优邮路P。其中改进Hungary算法是指改进了选取0元素的方法：通过选择0元素所在行(列)中0元素个数最少行(列)中的0元素，如果仍存在相同数量0元素的行(列)，再采用任意选取方法，从而避免了原始算法任意选取。元素而造成的死循环，也提高了算法的收敛性。采用上述中国邮路算法对车载设备模式转换有向图D进行遍历，生成的1条最优邮路P为P一SBSHSBSHSBFSSBOSSBCoSBCOSHTRPTSBCOFSSHTRPTSHTRPTFSOSSHISSBCO一0SFSCOTRPTFSCOT

27、RPTFSTRPTFSTRPTFSTRPTFSTRPTFSTRPTFSTRPTFSISSBCoTRPTOSCOTRPTOSTRPTOSTRPTOSTRPTOSTRPTOSISSBCOTRPTCoTRPTISSBCOISSBSLSBSLSBSLISSBTRISSB，ISSB因为最优邮路P的路径过长，所以要对P进行二次优化，即对P进行截断工作。与文献E8给出的二次优化方法不同，本文提出的二次优化方法只考虑对添加的重复路径进行截断。首先标记出添加的所有重复路径，根据规范对重复路径中的某些路径进行截断，将截断处的起点归于上一序列、终点归于下一个序列；其次，若重复路径属于重复的测试项，就删去起点和终点，

28、否则保留；最后，保证新序列的起点和终点均为SB模式。由此可生成9条测试目标序列，见表2。表2中：测试利用率为路径覆盖量占测试项的百分比；累计测试项为此测试目标序列之前包含的所有测试项数量；路径累计覆盖量为测试项之前包含的所有不重复的模式转换路径数量；累计测试利用率为路径累计覆盖量占累计测试项的百分比。由表2可知：测试目标序列3的测试利用率最高；随着测试目标序列号的增加，累计测试利用率越来越低，说明后续增加的测试序列中包含了很多重复的模式转换路径，降低了累计测试利用率，例如FS转TR的模式转换路径有6条，但是TR转PT的模式转换路径仅有1条，那么生成的测试目标序列不可避免地会存在多条TR转PT的

29、模式转换路径。表2生成的测试目标序列序号 测试目标序列 测紫7氅雾鬻帮甏紫燃霖黼SB+SH，s】+SH，SB+FS-SB+OS+1 SB+Co+SB+CoSH，TI卜，PT_+SBSB+COFsSHTRPTSHTR一“PTF+oS+SHISSB+C0卜OSFSCo-TR+PToFS。Co，TR+PTSB+F+TRPr-+FS+TRPrF+TR，PTsB一FS+TRPr-+FS+TRPT-+FS+。 TRPT-+F+ISSB+C0TR斗PT呻OSIC0斗TRPT一。 OS-TRPTSB一0STRPT一0STRPTOS一TRPT0S+ISSB+CoTR+PT+Co+TI卜，PT_+IS_+。SB+

30、Co+ISS昏+SL+SB+SL_+SB+SL一1s_+SB_+TR一。 IS+SB+IS+SB78891Ol0864639741561574964788766556532817O4O7122334455坫押卵蝎卵盯侣盯g；盯船卯“雅趵卵踮93韶伯鸥昌8万方数据第4期 基于有色Petri网的车载设备模式转换测试序列生成方法 1214测试序列集的选择性生成将生成的测试目标序列作为MTCPN模型的输入，仿真生成可执行测试序列集和XML文件集。采用该方法生成的测试序列集能够覆盖所有模式转换路径，满足全路径覆盖准则和CPN相应的覆盖标准，并且生成的测试序列容易为实际的测试执行。以表2中测试利用率最高的

31、测试目标序列3为例，首先约定SB模式的初始标记为1 7(6，true)，：1P-?：一 嚣二然后根据测试目标序列3驱动MTCPN模型的仿真；其次更改测试目标序列所涉及的库所颜色集，即更改为积颜色集INTMODEWRIECOMM，增加表示测试步骤的整数颜色集INT，得到对应的测试序列，如图7所示，因测试输人数据和测试输出数据已包含于每个变迁的守卫函数和执行函数中，所以此测试序列中包含测试步骤、测试输入数据及测试输出数据等，是可执行的测试序列。图7给出的测试序列3属于CPN模型，通过CPNTools工具内嵌的XML文件保存功能能够得到此序列的XML文件。”了“2。 “i：。；。o。；彝Q寡i乏憾Q

32、。9一瑚雾【一醺萝一J图7基于CPN的测试序列3将本文提出的车载设备转换模式测试序列生成方法与文献9中的2个生成方法进行对比，结果见表3。由表3可知：与文献E9相比，本文方法生成的测试序列总数、测试项数均较少，但测试利用率较高，说明本文方法提高了测试效率。表3生成方法的对比5结束语本文将车载设备模式转换理论与CPN建模方法有效融合，提出了基于CPN模型的车载设备模式转换测试序列生成方法。该方法根据规范，首先基于有色Petri网构建车载设备模式转换(MTCPN)模型，并采用ASKCTL逻辑公式对MTCPN模型进行验证；然后根据车载设备模式转换规则，将车载设备的工作模式及其转换路径映射为有向图，采

33、用中国邮路算法求解有向图，生成1条最优邮路，对该邮路进行二次优化，生成车载设备模式转换的测试目标序列集；将生成的浈4试目标序列作为MTCPN模型的输入，仿真生成满足全路径覆盖准则和CPN相应覆盖准则的可执行的测试序列集和XML文件集。该方法以实际数据驱动MTCPN模型，仿真生成i贝0试序列，保证了测试序列的可执行性，巧妙地避开了基于遍历模型状态空间的传统生成方法所存在的状态空间爆炸和死循环问题，为基于CPN的模式转换测试研究提供了1种新的思路与解决方案。参 考 文 献1李伟，王海峰CTCS-3级列控系统车载设备测试序列的优化J北京交通大学学报，2010，34(2)：7578(LI Wei，WA

34、NG HaifengOptimization Test Sequence of CTCS-3 On-Board EquipmentJJournal of Beijing Jiaotong University，2010，34(2)：7578in Chinese)2徐俊明图论及其应用M合肥：中国科学技术大学出版社，20103 张勇，王超琦CTCS-3级列控系统车载设备测试序列优化生成方法J中国铁道科学，201 1，32(3)：100106(ZHANG Yong，WANG ChaoqiThe Method for the Optimal Generation of Test Sequence fo

35、r CrC孓3 On-Board万方数据122 中国铁道科学 第38卷Equipment fJChina Railway Science，2011，32(3)：100106in Chinese)4张仕雄CTCS-3级列控系统测试序列合理性验证的研究J铁道标准设计，2012(12)：103105(ZHANG ShixiongStudy on Rationality Verification for CTCS-3 Train Control System Test SequencesJRailwayStandard Design，2012(12)：103105in Chinese)5LEDRU Y

36、，BOUSQUET L D，BONTRON P，et a1Test Purposes：Adapting the Notion of Specification to Testingc16th IEEE International Conference on Automated Software Engineering(ASE2001)San Diego：IEEE CSPress，2001：1271346颜炯，王戟，陈火旺基于模型的软件测试综述J计算机科学，2004，31(2)：184187(YAN Jiong，WANG Ji，CHEN HuowangSurvey of Model-Based

37、Software TestingJComputer Science，2004，31(2)：184187in Chinese)7UTTING M，LEGEARD BPractical Model-Based Testing：a Tools ApproachMSan Francisco：Morgan Kaufmann，20108赵显琼，唐涛多端口形式化测试自动生成方法在CTCS-3车载系统中的应用J铁道学报，2011，33(7)：4451(ZHA0 Xianqiong，TANG TaoMultiPort Based Automatic Formal Testing Generation and I

38、ts Application inCTCS-3 Level On-Board SystemJJournal of the China Railway Society，2011，33(7)：4451in Chinese)9袁磊，吕继东，刘雨，等一种全覆盖的列控车载系统测试用例自动生成算法研究fJ铁道学报，2014，36(8)：5562(YUAN Lei，LU Jidong，LIU Yu，et a1Research on ModelBased Test Case Generation Method of OnboardSubsystem in CTCS-3 I-JJournal of the Ch

39、ina Railway Society，2014，36(8)：5562in Chinese)10陈鑫，姜鹏，张一帆，等一种面向列车控制系统中安全攸关场景的测试用例自动生成方法J软件学报，2015，26(2)：269278(CHEN Xin，JIANG Peng，ZHANG Yifan，et a1Method of the Automatic Test Case Generation for Safety-CriticalScenarios in Train Control Systems I-JJournal of Software，2015，26(2)：269278in Chinese)E1

40、1JENSEN KA Brief Introduction to Coloured Petri NetsCInternational Workshop on Tools and Algorithmsfor the Construction and Analysis of SystemsHeidelberg：Springer，1997：2003200812JENSEN K，KRISTENSEN L M，WELLS L Coloured Petri Nets and CPN Tools for Modeling and Validation ofCurrent Systems口Internatio

41、nal Journal on Software Tools for Technology Transfer，2007，9(34)：21325413JENSEN K，KRISTENSEN L M Coloured Petri Nets：Modeling and Validation of Concurrent SystemsMHeidelberg：Springer SciencesBusiness Media，2009E14牟小玲，丁晓明，张望基于Petri网的测试用例生成研究进展J重庆交通大学学报：自然科学版，2012，31(1)：163167(MU Xiaoling，DING Xiaomin

42、g，ZHANG WangResearch Progress in Test Case Generation Based on Petri NetsJJournal of Chongqing Jiaotong University：Natural Science，2012，31(1)：163167in Chinese)15刘婧，叶新铭，李军BitTorrent协议的Petri网建模方法研究J系统仿真学报，2011，23(11)：23122320(LIU Jing，YE Xinming，LI JurL Towards Formal Modeling Methodology of BitTorren

43、t Based on Petri NetsJJournal of System Simulation，2011，23(11)：23122320in Chinese)16马国富，刘文良，周建勇，等有色Petri网模型中死标志合理性分析与验证l-J计算机应用研究，2014，31(12)：36513654(MA Guofu，LIU Wenliang，ZHOU Jianyong，et a1Analysis and Verification of Rationality of Dead Markings inColored Petri Net ModelsJApplication Research of

44、 Computers，2014，31(12)：36513654in Chinese)17FAROOQ U，LAM C P，LI HTowards Automated Test Sequence Generation EcProceedings of the 19thAustralian Conference on Software EngineeringPerth，Australia：Conference on Software Engineering，2008：44145018LIU Jing，YE Xinming，ZHOU Jiantao，et a1IO ConfOrmance Test

45、Generation with Colored Petri NetsJApplied MathematicsInformation Sciences，2014，8(6)：26952704E19刘婧，李茹，叶新铭，等PN4TS：一种基于CPN模型的IOCO测试选择方法J计算机学报，2014，37(12)：245】一2463万方数据第4期 基于有色Petri网的车载设备模式转换测试序列生成方法 123I-203E213E2232324(LIU Jing，LI Ru，YE Xinming，et a1PN4TS：Test Selection Approach with IO(20 Based on C

46、olored Petri Nets口Chinese Journal of Computers，2014，37(12)：24512463in Chinese)赵显琼，郑伟，唐涛一种基于模型的形式化测试序列自动生成方法及在ETCS-2中的应用J铁道学报，2012，34(5)：7074(ZHAO Xianqiong，ZHENG Wei，TANG TaoModelBased Formal Approach for Generating Test Cases and TestSequences Automatically by Example of the ETCS-2JJournal of the C

47、hina Railway Society，2012，34(5)：7074in Chinese)ZHENG Wei，LIANG Ci，WANG Rui，et a1Automated Test Approach Based on All Paths Covered Optimal Algorithm and Sequence Priority Selected AlgorithmJIEEE Transactions on Intelligent Transportation Systems，2014，15(6)：25512559ZHENG WeiHU NaiwenAutomated Test Sequence Optimization Based on the Maze Algorithm and Ant ColonyAlgorithmJInternational Journal of Computers CommunicationsControl，2015，