安全計算機平臺測試序列的生成及應用.pdf

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

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

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