安全計(jì)算機(jī)平臺(tái)測(cè)試序列的生成及應(yīng)用.pdf

1、安全計(jì)算機(jī)平臺(tái)是軌道交通信號(hào)控制系統(tǒng)的核心基礎(chǔ)安全設(shè)備，通過(guò)測(cè)試來(lái)檢驗(yàn)安全計(jì)算機(jī)平臺(tái)是否能實(shí)現(xiàn)設(shè)計(jì)的安全功能是至關(guān)重要的。傳統(tǒng)的軟件測(cè)試方法存在諸多問(wèn)題，需要找到更為有效的，全面的測(cè)試方法。
　　本文引入了基于模型檢驗(yàn)的測(cè)試的概念，即用形式化的規(guī)范語(yǔ)言描述系統(tǒng)功能需求，再利用時(shí)態(tài)邏輯公式描述系統(tǒng)的性質(zhì)并取反，以誘使模型檢驗(yàn)工具輸出不滿(mǎn)足這一性質(zhì)的序列形式的反例，那么這個(gè)反例就是滿(mǎn)足系統(tǒng)性質(zhì)的一段測(cè)試序列?；谶@種形式化方法產(chǎn)生的測(cè)

2、試序列是模型檢驗(yàn)工具根據(jù)自身的算法生成，很大程度上避免了人為失誤，并且提高了測(cè)試的效率及測(cè)試序列的完備性。
　　首先，給出了基于模型檢驗(yàn)的測(cè)試序列生成及優(yōu)化方法。在描述符號(hào)模型檢驗(yàn)原理和CTL(計(jì)算樹(shù)邏輯，Computation Tree Logic)覆蓋標(biāo)準(zhǔn)的基礎(chǔ)上，通過(guò)分析測(cè)試序列的覆蓋范圍，證明了測(cè)試序列的覆蓋完整性。通過(guò)分析生成測(cè)試序列的有限計(jì)算樹(shù)，提出了測(cè)試序列的優(yōu)化算法，并給出了其高效性證明。
　　其次，生成和優(yōu)

3、化了安全計(jì)算機(jī)平臺(tái)測(cè)試序列。在描述安全計(jì)算機(jī)平臺(tái)結(jié)構(gòu)、應(yīng)用處理機(jī)和熱備管理單元功能的基礎(chǔ)上，根據(jù)有限狀態(tài)機(jī)與SMV(符號(hào)模型檢驗(yàn)，Symbolic Model Verifying)語(yǔ)言的轉(zhuǎn)換規(guī)則，對(duì)安全計(jì)算機(jī)平臺(tái)模型進(jìn)行了形式化描述。進(jìn)而通過(guò)模型檢驗(yàn)工具NuSMV和構(gòu)建的安全計(jì)算機(jī)平臺(tái)測(cè)試覆蓋標(biāo)準(zhǔn)，得出了應(yīng)用處理機(jī)和熱備管理單元的測(cè)試序列并給出了上述兩種測(cè)試序列的優(yōu)化結(jié)果。
　　最后，搭建了安全計(jì)算機(jī)平臺(tái)自動(dòng)測(cè)試系統(tǒng)。完成了測(cè)試上