基于有色Petri網的車載設備模式轉換測試序列生成方法

趙曉宇，楊志杰，呂旌陽

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

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

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

相對于其他形式化語言，有色Petri網(CPN)[11-13]具有直觀的圖形表示和嚴密的數學基礎，在描述系統(tǒng)的分叉、同步和并行等行為、層次化建模及處理數據方面具有很大優(yōu)勢；牟小玲[14]分析了目前基于Petri網的測試用例生成方法，并指出了未來研究方向。在CPN的建模方面，劉婧[15]針對BitTorrent協(xié)議的高并發(fā)性和交互行為復雜性，給出了協(xié)議的CPN層次模型，充分利用了CPN在層次建模、復雜數據處理與模型檢驗的優(yōu)勢。在CPN的模型檢驗方面，馬國富[16]提出了1種基于ASK-CTL及模型檢驗理論的死標志合理性驗證算法。在基于CPN的測試研究方面，Farooq[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)搜索算法實現轉換路徑全覆蓋的困難。相比而言，基于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)根據《規(guī)范》，基于CPN構建車載設備模式轉換(簡稱為MTCPN)模型，并采用ASK-CTL公式和非標準狀態(tài)空間查詢法對MTCPN模型進行分析與驗證。

(2)根據《規(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)Σ為有限非空的顏色集合，用于定義模型中的數據類型；V為變量集合；且滿足Type[v]?Σ,v∈V。

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

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

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

(6)I(I:P→EXPRΦ)為初始化賦值函數，用于定義庫所的初始數據賦值，滿足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}為端口類型函數，用于定義端口位置；Pport表示3種端口類型：輸入端口{IN}、輸出端口{OUT}和輸入輸出端口{I/O}。

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

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

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

定義4：ASK-CTL狀態(tài)公式表示如下，其中各參數的定義見文獻[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)公式的語義如下，其中各參數的定義見文獻[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模型的構建

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

表1　車載設備的模式轉換路徑數量表

根據《規(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ī)則，以輔助算法實現。

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

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

圖2　MTCPN模型的上層模型

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

2.2　MTCPN模型的驗證

模型驗證的基本思想是用狀態(tài)遷移系統(tǒng)表示系統(tǒng)的行為，用模態(tài)/時序邏輯公式描述系統(tǒng)的性質。Cheng等人將CPN與模型檢驗相結合，并在CPN Tools工具中引入了1種擴展邏輯語言ASK-CTL[24]。本節(jié)根據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模型的測試生成方法，大多數以空間搜索算法為基礎，但這類方法容易陷入死循環(huán)，并且由于車載設備模式轉換的復雜性，更加劇了模式轉換測試序列實現轉換路徑全覆蓋的困難。為了解決上述問題，針對《規(guī)范》采用中國郵路算法生成測試目標序列。

根據車載設備模式轉換規(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元素個數最少行(列)中的0元素，如果仍存在相同數量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)化方法只考慮對添加的重復路徑進行截斷。首先標記出添加的所有重復路徑，根據《規(guī)范》對重復路徑中的某些路徑進行截斷，將截斷處的起點歸于上一序列、終點歸于下一個序列；其次，若重復路徑屬于重復的測試項，就刪去起點和終點，否則保留；最后，保證新序列的起點和終點均為SB模式。

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

表2　生成的測試目標序列

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

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

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

圖7　基于CPN的測試序列3

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

表3　生成方法的對比

5　結束語

本文將車載設備模式轉換理論與CPN建模方法有效融合，提出了基于CPN模型的車載設備模式轉換測試序列生成方法。該方法根據《規(guī)范》，首先基于有色Petri網構建車載設備模式轉換(MTCPN)模型，并采用ASK-CTL邏輯公式對MTCPN模型進行驗證；然后根據車載設備模式轉換規(guī)則，將車載設備的工作模式及其轉換路徑映射為有向圖，采用中國郵路算法求解有向圖，生成1條最優(yōu)郵路，對該郵路進行二次優(yōu)化，生成車載設備模式轉換的測試目標序列集；將生成的測試目標序列作為MTCPN模型的輸入，仿真生成滿足全路徑覆蓋準則和CPN相應覆蓋準則的可執(zhí)行的測試序列集和XML文件集。該方法以實際數據驅動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網的測試用例生成研究進展[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網建模方法研究[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網模型中死標志合理性分析與驗證[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.