CTCS-3級(jí)測試案例完備性的自動(dòng)驗(yàn)證.pdf

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

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

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

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