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

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

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

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

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