CTCS-3級測試案例完備性的自動驗證.pdf

1、CTCS-3級列控系統(tǒng)作為確保高速鐵路系統(tǒng)高效、安全運營的關(guān)鍵，有著極其嚴格安全性、可靠性要求。為了確保CTCS-3級列控系統(tǒng)滿足《CTCS-3級列控系統(tǒng)需求規(guī)范(SRS)(v1.0)》中規(guī)定的功能需求，需要對其進行充分的測試，而《CTCS-3級列控系統(tǒng)測試案例(v3.0)》構(gòu)成了測試過程的基礎(chǔ)和標準。測試案例的完備性，即測試案例的設(shè)計可以覆蓋全部的系統(tǒng)功能需求，是測試過程能夠充分驗證列控系統(tǒng)是否符合SRS規(guī)定的關(guān)鍵。因此，為了確保測試

2、案例的完備性，本文提出了一種CTCS-3級列控系統(tǒng)測試案例完備性的驗證方法。
　　論文的主要工作如下:
　　(1)對CTCS-3級列控系統(tǒng)的測試過程以及測試案例的生成方法和描述形式進行研究，明確了CTCS-3級列控系統(tǒng)測試案例完備性驗證的主要需求，以及需要解決的關(guān)鍵問題。
　　(2)通過對關(guān)鍵問題的分析，提出基于Event-B和因果圖法的測試案例完備性驗證方法。利用Event-B方法對SRS進行嚴格的形式化建模，并將建

3、模結(jié)果轉(zhuǎn)換為因果圖形式，通過生成SRS判定表并對測試案例進行因果圖建模和判定表生成，統(tǒng)一SRS和測試案例的描述方式，同時依據(jù)SRS判定表得到測試案例的完備性衡量依據(jù)，最終通過對比驗證得出測試案例的完備性驗證結(jié)果。
　　(3)在對上述方法進行詳細設(shè)計的過程中，為了實現(xiàn)模型轉(zhuǎn)換，設(shè)計了Event-B模型的改寫、映射規(guī)則;為了明確SRS和測試案例的對應關(guān)系，提出了利用SRS因果圖模型內(nèi)事件對測試案例進行建模的方法，并相應設(shè)計了基于SRS

4、判定表的測試充分性準則和覆蓋域;根據(jù)測試案例判定表和覆蓋域，設(shè)計了測試案例完備性的對比驗證流程，使驗證結(jié)果便于工作人員的使用。
　　(4)在設(shè)計上述測試案例完備性驗證方法的基礎(chǔ)上，結(jié)合Rodin建模平臺設(shè)計并開發(fā)了CTCS-3級列控系統(tǒng)測試案例完備性的自動驗證工具。利用車載設(shè)備待機模式下的模式轉(zhuǎn)換功能和RBC切換功能的相關(guān)測試案例作為實例，應用自動驗證工具對其進行了完備性驗證，發(fā)現(xiàn)了現(xiàn)有測試案例中可能存在的不足并提出了處理建議，驗