趙曉宇，楊志杰，呂旌陽

(1.中國鐵道科學研究院 研究生部，北京　100081；2.中國鐵道科學研究院 通信信號研究所，北京　100081；3.中國鐵道科學研究院 國家鐵路智能運輸系統(tǒng)工程技術研究中心，北京　100081；4.北京郵電大學 信息與通信工程學院，北京　100876)

CTCS-3級列控系統(tǒng)由車載設備和地面設備組成，屬于典型的安全苛求系統(tǒng)。為了驗證其行為功能的正確性，并保證不同廠家設備的兼容性，對其系統(tǒng)的功能進行測試成為必不可少的環(huán)節(jié)。如何高效地自動生成覆蓋車載設備所有轉換路徑的測試序列，是目前車載設備模式轉換測試的關鍵性問題?，F(xiàn)有測試方法以人工測試和現(xiàn)場測試為主，測試時間較長，測試費用昂貴，導致測試效率較低，并且在很多情況下已經(jīng)無法滿足測試的需求。在這種背景下，自動測試方法應運而生。

針對車載設備模式轉換功能的測試序列生成問題，李偉[1]將其轉化為中國郵路問題[2]，使用遺傳算法生成測試序列；張勇[3]采用Edmonds-Johnson算法及LINGO工具解決測試序列生成問題；但文獻[1,3]都未涉及具體的測試序列生成過程，僅給出了車載設備模式轉換的測試順序。測試序列的合理性驗證方面，張仕雄[4]對CTCS-3級列控系統(tǒng)測試序列的合理性進行了驗證，但僅對序列合理性進行了初步分析。近年來，基于模型的測試方法[5-7]有效地融合了形式化方法與傳統(tǒng)測試技術，在形式化建模方法的基礎上，自動生成大量可靠的測試用例，提高了人工編寫測試用例的效率，縮短了與自動化程度較高的測試執(zhí)行過程的距離?；谀Ｐ偷牧锌叵到y(tǒng)測試方面，趙顯瓊[8]針對多端口協(xié)同測試問題提出了端口標記的時間輸入輸出自動機(LpTIOA)；袁磊[9]提出了1種能夠滿足全狀態(tài)、全變遷覆蓋準則的測試套自動生成算法；并且文獻[8—9]均通過UPPAAL和CoVer工具生成滿足相應覆蓋標準的測試套，但生成的測試套抽象層次太高，無法描述系統(tǒng)的并發(fā)行為；姜鵬[10]根據(jù)安全苛求攸關場景建模需求，擴充了UML的事件驅動機制和時間特性描述機制，并提出了1種面向安全攸關場景的測試用例自動生成方法，但UML無法描述系統(tǒng)的并發(fā)行為，不能進行模型檢驗，具有一定的局限性。

相對于其他形式化語言，有色Petri網(wǎng)(CPN)[11-13]具有直觀的圖形表示和嚴密的數(shù)學基礎，在描述系統(tǒng)的分叉、同步和并行等行為、層次化建模及處理數(shù)據(jù)方面具有很大優(yōu)勢；牟小玲[14]分析了目前基于Petri網(wǎng)的測試用例生成方法，并指出了未來研究方向。在CPN的建模方面，劉婧[15]針對BitTorrent協(xié)議的高并發(fā)性和交互行為復雜性，給出了協(xié)議的CPN層次模型，充分利用了CPN在層次建模、復雜數(shù)據(jù)處理與模型檢驗的優(yōu)勢。在CPN的模型檢驗方面，馬國富[16]提出了1種基于ASK-CTL及模型檢驗理論的死標志合理性驗證算法。在基于CPN的測試研究方面，F(xiàn)arooq[17]提出了基于控制流的測試序列生成方法，通過隨機漫步算法對CPN模型的狀態(tài)空間進行多次搜索，生成滿足覆蓋標準的測試例集合，但容易生成冗余的測試案例；劉婧[18]研究了基于CPN的輸入輸出一致性測試(IOCO)生成方法，并給出了1種基于CPN描述測試目的模型并驅動IOCO一致性測試選擇的新方法[19]；趙顯瓊[20]給出了基于CPN的測試案例自動生成算法和測試序列搜索算法；鄭偉[21]對測試案例生成算法[20]進行了改進，提出了基于CPN的全路徑覆蓋優(yōu)化算法和序列優(yōu)選算法，后又提出了基于改進蟻群算法的測試序列生成方法[22]，用于提高自動測試執(zhí)行的效率?？傮w而言，這些研究均采用啟發(fā)式搜索算法生成測試用例，容易造成狀態(tài)空間爆炸和死循環(huán)問題。同時，車載設備模式轉換的復雜性，增加了傳統(tǒng)搜索算法實現(xiàn)轉換路徑全覆蓋的困難。相比而言，基于CPN的模擬仿真，屬于狀態(tài)空間的動態(tài)探索分析，是解決狀態(tài)空間爆炸和死循環(huán)的有效途徑。因此，本文基于《CTCS-3級列控系統(tǒng)系統(tǒng)需求規(guī)范(SRS)》[23](簡稱《規(guī)范》)，針對車載設備模式轉換的功能，提出基于CPN的車載設備模式轉換測試序列生成方法。

1　基于CPN的車載設備模式轉換測試序列生成方法

1.1　方法的總體框架

基于CPN的車載設備模式轉換測試序列生成方法的總體框架如圖1所示，包括如下3個部分。

(1)根據(jù)《規(guī)范》，基于CPN構建車載設備模式轉換(簡稱為MTCPN)模型，并采用ASK-CTL公式和非標準狀態(tài)空間查詢法對MTCPN模型進行分析與驗證。

(2)根據(jù)《規(guī)范》，采用中國郵路算法生成車載設備模式轉換的測試目標序列。

(3)將生成的測試目標序列作為MTCPN模型的輸入，仿真生成滿足全路徑覆蓋準則和CPN相應覆蓋準則的可執(zhí)行的測試序列集和XML文件集，避免了采用啟發(fā)式搜索算法導致的狀態(tài)空間爆炸和死循環(huán)問題。

圖1基于CPN的車載設備模式轉換測試序列生成方法框架圖

1.2相關定義

定義1：非層次化CPN模型采用9個元素表示，即CPN=(P,T,A,Σ,V,C,G,E,I)，其中各個元素的含義如下。

(1)P為庫所的有限集合；T為變遷的有限集合；A為弧的有限集合；且滿足P∩T=P∩A=T∩A=?，A?P×T∩T×P。

(2)Σ為有限非空的顏色集合，用于定義模型中的數(shù)據(jù)類型；V為變量集合；且滿足Type[v]?Σ,v∈V。

(3)C(C:P→Σ)為著色函數(shù)，用于定義庫所上允許的顏色類型，即從庫所P到顏色集Σ的映射。

(4)G(G:T→EXPRv)為守衛(wèi)表達式函數(shù)，用于定義變遷上的守衛(wèi)函數(shù)，給出了變遷的點火條件。

(5)E(E:A→EXPRv)為弧表達式函數(shù)，用于定義弧上的弧函數(shù)，滿足Type[E(a)]=C(p)MS，即與弧連接的庫所的著色函數(shù)約束著弧表達式的數(shù)據(jù)類型，其中CMS為集合C的多重集集合。

(6)I(I:P→EXPRΦ)為初始化賦值函數(shù)，用于定義庫所的初始數(shù)據(jù)賦值，滿足Type[I(p)]=C(p)MS。

定義2：CPN模塊采用4個元素表示，即CPNM=(CPN,Pport,Tsub,PT)，其中各個元素的含義如下。

(1)CPN為一個非層次化CPN模型。

(2)Pport?P為端口位置集合；Tsub?T為替代變遷集合。

(3)PT:Pport→{IN,OUT,I/O}為端口類型函數(shù)，用于定義端口位置；Pport表示3種端口類型：輸入端口{IN}、輸出端口{OUT}和輸入輸出端口{I/O}。

定義3：層次化CPN模型采用4個元素表示，即CPNH=(S,SM,PS,FS)，其中各個元素的含義如下。

(2)SM:Tsub→S為子模塊函數(shù)，用于關聯(lián)替代變遷和對應的CPN模塊。

(4)FS?2p是庫所融合集，滿足?(p,p′)∈fs,fs∈FS,C(p)=C(p′),I(p)<>=I(p′)<>，即庫所融合集中的所有庫所是相通的。

定義4：ASK-CTL狀態(tài)公式表示如下，其中各參數(shù)的定義見文獻[24]。

A::=tt|α|┐A|A1∨A2||EU(A1,

A2)|AU(A1,A2)

=tt|α|NOT(A)|A1∪A2||EU(A1,A2)|AU(A1,A2)

定義5：ASK-CTL狀態(tài)公式的語義如下，其中各參數(shù)的定義見文獻[24]。

(1)og,v|=Sttt總是為真；

(2)og,v|=Stα，iifα在節(jié)點v上為真；

(3)og,v|=St┐A=NOT(A)，iif not

og,v|=StA；

(4)og,v|=StA1∨A2=A1∪A2，iifog,

v|=StA1orog,v|=StA2；

(5)og,v|=St，iif ?a=

(s,(t,b),s′)∈A∩a|=TrB；

(6)og,v|=StEU(Ai,Aj)， iif

?π∈vPaths(s):?j:?0≤i≤j:og,

π(vi)|=StA1∧?i≥j:og,π(vi)|=StA2；

(7)og,v|=StAU(Ai,Aj)，iff

?π∈vPaths(v):?j:?0≤i≤j:og,

π(vi)|=StA1∧?i≥j:og,π(vi)|=StA2。

ASK-CTL的變遷公式和語義也見文獻[24]。

2　MTCPN模型的構建和驗證

2.1　MTCPN模型的構建

根據(jù)《規(guī)范》可知：CTCS-3級列控車載設備有9種工作模式，即完全監(jiān)控模式(FS)、目視行車模式(OS)、引導模式(CO)、調(diào)車模式(SH)、隔離模式(IS)、待機模式(SB)、冒進防護模式(TR)、冒進后防護模式(PT)和休眠模式(SL)；且車載設備各工作模式之間存在的轉換條件(即轉換路徑)數(shù)量見表1。

表1　車載設備的模式轉換路徑數(shù)量表

根據(jù)《規(guī)范》，提出以下8條建模規(guī)則。

(1)采用分層(2層)建模規(guī)則構建MTCPN模型，上層模型只考慮各模式之間的轉換路徑，下層模型考慮各模式轉換的具體轉換流程。

(2)《規(guī)范》中的“轉換條件18”是針對CTCS-2等級的，本文不做討論。

(3)為使MTCPN模型簡潔且不失普遍性，除SH，IS和SL模式外，默認其他模式均與RBC已建立通信會話，并且只考慮各模式轉換流程，對模式轉換后的流程不做處理。

(4)為使MTCPN模型便于分析，凡是跟應答器相關的流程，均按照單個應答器處理。

(5)建模過程嚴格遵守車載設備模式轉換規(guī)范，暫不考慮特殊情況。

(6)MTCPN上層模型的模式轉換均用替代變遷表示，具體的轉換流程均在MTCPN下層模型表示。

(7)MTCPN模型中，顏色的定義、變量和庫所等的命名均遵循一定的規(guī)則，以輔助算法實現(xiàn)。

(8)對數(shù)據(jù)內(nèi)容的判斷行為，均在守衛(wèi)函數(shù)中體現(xiàn)。

由此構建出MTCPN模型。其中，上層模型如圖2所示；下層模型共有39個，這里僅給出其中SB模式轉FS模式的下層模型，如圖3所示。

圖2　MTCPN模型的上層模型

圖3　SB模式轉FS模式的下層模型

2.2　MTCPN模型的驗證

模型驗證的基本思想是用狀態(tài)遷移系統(tǒng)表示系統(tǒng)的行為，用模態(tài)/時序邏輯公式描述系統(tǒng)的性質(zhì)。Cheng等人將CPN與模型檢驗相結合，并在CPN Tools工具中引入了1種擴展邏輯語言ASK-CTL[24]。本節(jié)根據(jù)CPN模型檢測理論，使用分支時序邏輯ASK-CTL公式及非標準狀態(tài)空間查詢法對構建的MTCPN模型進行驗證。

針對圖2進行MTCPN模型的死鎖分析，其結果如圖4所示，可知MTCPN模型無死標識節(jié)點，屬于強連通圖，說明構建的MTCPN模型滿足《規(guī)范》要求的模式轉換功能。

圖4　MTCPN模型的死鎖分析結果

針對圖3進行轉換規(guī)則的驗證，其結果如圖5所示。實際測試的車載流程中，車載設備的初始工作模式始終為SB模式，即庫所SB的初始標記為1′(6,true)(變量“6”表示M_MODE=6，即車載模式為SB模式，變量“true”表示B_WrieComm=true，即SB模式下車載設備已與無線閉塞中心RBC建立了通信連接，那么存在某條路徑，使得SB模式可轉入FS模式；同理，存在某條路徑，使得FS模式可轉入TR模式，執(zhí)行ASL-CTL公式，返回執(zhí)行結果“true”，如圖5(a)所示；如果刪除庫所SB的初始標記，其返回結果如圖5(b)所示，表示這種情況永遠不會發(fā)生；如果設置庫所FS的初始標記為1′(0,true)，其執(zhí)行結果同樣如圖5(a)所示，說明構建的MTCPN模型符合車載設備模式轉換流程。

圖5　模式轉換規(guī)則的驗證結果

3　測試目標序列集的生成方法

對于傳統(tǒng)的基于CPN模型的測試生成方法，大多數(shù)以空間搜索算法為基礎，但這類方法容易陷入死循環(huán)，并且由于車載設備模式轉換的復雜性，更加劇了模式轉換測試序列實現(xiàn)轉換路徑全覆蓋的困難。為了解決上述問題，針對《規(guī)范》采用中國郵路算法生成測試目標序列。

根據(jù)車載設備模式轉換規(guī)則，將車載設備的工作模式映射成有向圖的頂點，車載設備的模式轉換路徑映射成有向圖的弧，則可將表1轉換成有向圖D，如圖6所示。

圖6　車載設備模式轉換有向圖

由圖6和第2.2節(jié)可知，映射后的車載設備模式轉換有向圖為強連通圖，即車載設備模式轉換有向圖存在最優(yōu)郵路，因此采用中國郵路算法生成測試目標序列，算法步驟如下。

步驟3：利用Floyd算法求解各個頂點(vi,vj)間的最短距離矩陣F與最短路徑矩陣P′。

步驟5：對平衡歐拉圖D′進行歐拉尋址，得到最優(yōu)郵路P。

其中改進Hungary算法是指改進了選取0元素的方法：通過選擇0元素所在行(列)中0元素個數(shù)最少行(列)中的0元素，如果仍存在相同數(shù)量0元素的行(列)，再采用任意選取方法，從而避免了原始算法任意選取0元素而造成的死循環(huán)，也提高了算法的收斂性。

采用上述中國郵路算法對車載設備模式轉換有向圖D進行遍歷，生成的1條最優(yōu)郵路P為

P={SB→SH→SB→SH→SB→FS→

SB→OS→SB→CO→SB→CO→

SH→TR→PT→SB→CO→FS→

SH→TR→PT→SH→TR→PT→

FS→OS→SH→IS→SB→CO→

OS→FS→CO→TR→PT→FS→

CO→TR→PT→FS→TR→PT→

FS→TR→PT→FS→TR→PT→

FS→TR→PT→FS→TR→PT→

FS→TR→PT→FS→IS→SB→

CO→TR→PT→OS→CO→TR→

PT→OS→TR→PT→OS→TR→

PT→OS→TR→PT→OS→TR→

PT→OS→IS→SB→CO→TR→

PT→CO→TR→PT→IS→SB→

CO→IS→SB→SL→SB→SL→

SB→SL→IS→SB→TR→IS→

SB→IS→SB}

因為最優(yōu)郵路P的路徑過長，所以要對P進行二次優(yōu)化，即對P進行截斷工作。與文獻[3]給出的二次優(yōu)化方法不同，本文提出的二次優(yōu)化方法只考慮對添加的重復路徑進行截斷。首先標記出添加的所有重復路徑，根據(jù)《規(guī)范》對重復路徑中的某些路徑進行截斷，將截斷處的起點歸于上一序列、終點歸于下一個序列；其次，若重復路徑屬于重復的測試項，就刪去起點和終點，否則保留；最后，保證新序列的起點和終點均為SB模式。

由此可生成9條測試目標序列，見表2。表2中：測試利用率為路徑覆蓋量占測試項的百分比；累計測試項為此測試目標序列之前包含的所有測試項數(shù)量；路徑累計覆蓋量為測試項之前包含的所有不重復的模式轉換路徑數(shù)量；累計測試利用率為路徑累計覆蓋量占累計測試項的百分比。由表2可知：測試目標序列3的測試利用率最高；隨著測試目標序列號的增加，累計測試利用率越來越低，說明后續(xù)增加的測試序列中包含了很多重復的模式轉換路徑，降低了累計測試利用率，例如FS轉TR的模式轉換路徑有6條，但是TR轉PT的模式轉換路徑僅有1條，那么生成的測試目標序列不可避免地會存在多條TR轉PT的模式轉換路徑。

表2　生成的測試目標序列

4　測試序列集的選擇性生成

將生成的測試目標序列作為MTCPN模型的輸入，仿真生成可執(zhí)行測試序列集和XML文件集。采用該方法生成的測試序列集能夠覆蓋所有模式轉換路徑，滿足全路徑覆蓋準則和CPN相應的覆蓋標準，并且生成的測試序列容易為實際的測試執(zhí)行。

以表2中測試利用率最高的測試目標序列3為例，首先約定SB模式的初始標記為1′(6,true)，然后根據(jù)測試目標序列3驅動MTCPN模型的仿真；其次更改測試目標序列所涉及的庫所顏色集，即更改為積顏色集INT×MODE×WRIECOMM，增加表示測試步驟的整數(shù)顏色集INT，得到對應的測試序列，如圖7所示，因測試輸入數(shù)據(jù)和測試輸出數(shù)據(jù)已包含于每個變遷的守衛(wèi)函數(shù)和執(zhí)行函數(shù)中，所以此測試序列中包含測試步驟、測試輸入數(shù)據(jù)及測試輸出數(shù)據(jù)等，是可執(zhí)行的測試序列。圖7給出的測試序列3屬于CPN模型，通過CPN Tools工具內(nèi)嵌的XML文件保存功能能夠得到此序列的XML文件。

圖7　基于CPN的測試序列3

將本文提出的車載設備轉換模式測試序列生成方法與文獻[9]中的2個生成方法進行對比，結果見表3。由表3可知：與文獻[9]相比，本文方法生成的測試序列總數(shù)、測試項數(shù)均較少，但測試利用率較高，說明本文方法提高了測試效率。

表3　生成方法的對比

5　結束語

本文將車載設備模式轉換理論與CPN建模方法有效融合，提出了基于CPN模型的車載設備模式轉換測試序列生成方法。該方法根據(jù)《規(guī)范》，首先基于有色Petri網(wǎng)構建車載設備模式轉換(MTCPN)模型，并采用ASK-CTL邏輯公式對MTCPN模型進行驗證；然后根據(jù)車載設備模式轉換規(guī)則，將車載設備的工作模式及其轉換路徑映射為有向圖，采用中國郵路算法求解有向圖，生成1條最優(yōu)郵路，對該郵路進行二次優(yōu)化，生成車載設備模式轉換的測試目標序列集；將生成的測試目標序列作為MTCPN模型的輸入，仿真生成滿足全路徑覆蓋準則和CPN相應覆蓋準則的可執(zhí)行的測試序列集和XML文件集。該方法以實際數(shù)據(jù)驅動MTCPN模型，仿真生成測試序列，保證了測試序列的可執(zhí)行性，巧妙地避開了基于遍歷模型狀態(tài)空間的傳統(tǒng)生成方法所存在的狀態(tài)空間爆炸和死循環(huán)問題，為基于CPN的模式轉換測試研究提供了1種新的思路與解決方案。

[1]李偉, 王海峰. CTCS-3級列控系統(tǒng)車載設備測試序列的優(yōu)化[J]. 北京交通大學學報, 2010, 34(2): 75-78.

(LI Wei, WANG Haifeng. Optimization Test Sequence of CTCS-3 On-Board Equipment [J]. Journal of Beijing Jiaotong University, 2010, 34(2): 75-78. in Chinese)

[2]徐俊明. 圖論及其應用[M]. 合肥: 中國科學技術大學出版社，2010.

[3]張勇, 王超琦. CTCS-3級列控系統(tǒng)車載設備測試序列優(yōu)化生成方法[J]. 中國鐵道科學, 2011, 32(3): 100-106.

(ZHANG Yong, WANG Chaoqi. The Method for the Optimal Generation of Test Sequence for CTCS-3 On-Board Equipment [J]. China Railway Science, 2011, 32(3): 100-106. in Chinese)

[4]張仕雄. CTCS-3級列控系統(tǒng)測試序列合理性驗證的研究[J]. 鐵道標準設計, 2012(12):103-105.

(ZHANG Shixiong. Study on Rationality Verification for CTCS-3 Train Control System Test Sequences [J]. Railway Standard Design, 2012 (12):103-105. in Chinese)

[5]LEDRU Y, BOUSQUET L D, BONTRON P, et al. Test Purposes: Adapting the Notion of Specification to Testing [C]//16th IEEE International Conference on Automated Software Engineering(ASE2001). San Diego: IEEE CS Press, 2001: 127-134.

[6]顏炯, 王戟, 陳火旺. 基于模型的軟件測試綜述[J]. 計算機科學, 2004, 31(2): 184-187.

(YAN Jiong, WANG Ji, CHEN Huowang. Survey of Model-Based Software Testing [J]. Computer Science, 2004, 31(2): 184-187. in Chinese.)

[7]UTTING M, LEGEARD B. Practical Model-Based Testing: a Tools Approach [M]. San Francisco: Morgan Kaufmann, 2010.

[8]趙顯瓊, 唐濤. 多端口形式化測試自動生成方法在CTCS-3車載系統(tǒng)中的應用[J]. 鐵道學報, 2011, 33(7): 44-51.

(ZHAO Xianqiong, TANG Tao. Multi-Port Based Automatic Formal Testing Generation and Its Application in CTCS-3 Level On-Board System [J]. Journal of the China Railway Society, 2011, 33(7): 44-51. in Chinese)

[9]袁磊, 呂繼東, 劉雨, 等. 一種全覆蓋的列控車載系統(tǒng)測試用例自動生成算法研究[J].鐵道學報, 2014, 36(8): 55-62.

(YUAN Lei, Lü Jidong, LIU Yu, et al. Research 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. in Chinese)

[10]陳鑫, 姜鵬, 張一帆, 等. 一種面向列車控制系統(tǒng)中安全攸關場景的測試用例自動生成方法[J]. 軟件學報, 2015, 26(2): 269-278.

(CHEN Xin, JIANG Peng, ZHANG Yifan, et al. Method of the Automatic Test Case Generation for Safety-Critical Scenarios in Train Control Systems[J]. Journal of Software, 2015, 26(2): 269-278. in Chinese)

[11]JENSEN K. A Brief Introduction to Coloured Petri Nets[C]// International Workshop on Tools and Algorithms for the Construction and Analysis of Systems. Heidelberg: Springer, 1997: 2003-2008.

[12]JENSEN K, KRISTENSEN L M, WELLS L. Coloured Petri Nets and CPN Tools for Modeling and Validation of Current Systems [J]. International Journal on Software Tools for Technology Transfer, 2007, 9(3/4): 213-254.

[13]JENSEN K, KRISTENSEN L M. Coloured Petri Nets: Modeling and Validation of Concurrent Systems [M]. Heidelberg: Springer Sciences & Business Media, 2009.

[14]牟小玲, 丁曉明, 張望. 基于Petri網(wǎng)的測試用例生成研究進展[J]. 重慶交通大學學報:自然科學版, 2012, 31(1): 163-167.

(MU Xiaoling, DING Xiaoming, ZHANG Wang. Research Progress in Test Case Generation Based on Petri Nets [J]. Journal of Chongqing Jiaotong University:Natural Science, 2012, 31(1): 163-167. in Chinese)

[15]劉婧, 葉新銘, 李軍. BitTorrent協(xié)議的Petri網(wǎng)建模方法研究[J]. 系統(tǒng)仿真學報, 2011, 23(11): 2312-2320.

(LIU Jing, YE Xinming, LI Jun. Towards Formal Modeling Methodology of BitTorrent Based on Petri Nets [J]. Journal of System Simulation, 2011, 23(11): 2312-2320. in Chinese)

[16]馬國富, 劉文良, 周建勇, 等. 有色Petri網(wǎng)模型中死標志合理性分析與驗證[J]. 計算機應用研究, 2014, 31(12): 3651-3654.

(MA Guofu, LIU Wenliang, ZHOU Jianyong, et al. Analysis and Verification of Rationality of Dead Markings in Colored Petri Net Models [J]. Application Research of Computers, 2014, 31(12): 3651-3654. in Chinese)

[17]FAROOQ U, LAM C P, LI H. Towards Automated Test Sequence Generation[C]//Proceedings of the 19th Australian Conference on Software Engineering. Perth, Australia: Conference on Software Engineering，2008:441-450.

[18]LIU Jing, YE Xinming, ZHOU Jiantao，et al. I/O Conformance Test Generation with Colored Petri Nets [J]. Applied Mathematics & Information Sciences, 2014, 8(6): 2695-2704.

[19]劉婧, 李茹, 葉新銘, 等. PN4TS:一種基于CPN模型的IOCO測試選擇方法[J]. 計算機學報, 2014, 37(12): 2451-2463.

(LIU Jing, LI Ru, YE Xinming, et al. PN4TS: Test Selection Approach with IOCO Based on Colored Petri Nets [J]. Chinese Journal of Computers, 2014, 37(12): 2451-2463. in Chinese)

[20]趙顯瓊, 鄭偉, 唐濤. 一種基于模型的形式化測試序列自動生成方法及在ETCS-2中的應用[J]. 鐵道學報, 2012, 34(5): 70-74.

(ZHAO Xianqiong, ZHENG Wei, TANG Tao. Model-Based Formal Approach for Generating Test Cases and Test Sequences Automatically by Example of the ETCS-2 [J]. Journal of the China Railway Society, 2012, 34(5): 70-74. in Chinese)

[21]ZHENG Wei, LIANG Ci, WANG Rui, et al. Automated Test Approach Based on All Paths Covered Optimal Algorithm and Sequence Priority Selected Algorithm [J].IEEE Transactions on Intelligent Transportation Systems, 2014, 15(6): 2551-2559.

[22]ZHENG Wei, HU Naiwen. Automated Test Sequence Optimization Based on the Maze Algorithm and Ant Colony Algorithm [J]. International Journal of Computers Communications & Control, 2015, 10(4): 593-606.

[23]中華人民共和國鐵道部. 鐵科運[2008]127號 CTCS-3級列控系統(tǒng)系統(tǒng)需求規(guī)范(SRS)(V1.0)[S]. 北京: 中華人民共和國鐵道部, 2008.

[24]University of Aarhus. Design/CPN ASK-CTL Manual [EB/OL]. 1996. http://www.daimi.au.dk/designCPN/libs/askctl/ASKCTLmanual.pdf.