基于UPPAAL的計算機聯(lián)鎖進路控制過程測試用例自動生成.pdf

1、計算機聯(lián)鎖系統(tǒng)是保證列車在車站內(nèi)安全運行的重要手段，聯(lián)鎖邏輯運算的安全性和可靠性影響著整個車站設(shè)備的實時狀態(tài)，對行車安全有著至關(guān)重要的作用。因此需要對聯(lián)鎖系統(tǒng)軟件設(shè)計進行安全性測試。然而由于各個信號廠商軟件的不統(tǒng)一性，造成測試的難度很大。目前軟件的測試方法主要以代碼為中心來設(shè)計測試用例，系統(tǒng)測試的通用性和靈活性不足，由于對于同一個問題針對不同的開發(fā)人員編寫的程序和框架思路不完全一樣，就需要針對每行代碼或者每個模塊設(shè)計測試用例，測試效率極

2、低而且費時較多。
　　本文結(jié)合計算機聯(lián)鎖技術(shù)規(guī)范，深入分析了聯(lián)鎖內(nèi)部邏輯運算的核心過程，并引入人環(huán)因素的影響，分模塊建立計算機聯(lián)鎖狀態(tài)機模型，并對模型進行仿真和驗證，生成最終的測試用例。
　　首先從功能需求和人環(huán)因素兩個方面展開研究，將自然偶發(fā)因素和人為因素產(chǎn)生的設(shè)備故障對聯(lián)鎖運算的影響引入到聯(lián)鎖核心運算進路控制功能中。在系統(tǒng)需求分析的基礎(chǔ)上，利用UPPAAL軟件依據(jù)聯(lián)鎖邏輯過程對進路控制模塊進行建模，包括進路建立、進路正常

3、解鎖、調(diào)車中途折返解鎖、進路取消、人工解鎖和故障解鎖。其次采用UPPAAL的仿真環(huán)境和BNF語法以具體進路為例對建立的模型進行仿真和驗證，確保模型的正確性，并以XML文件保存了模型中狀態(tài)和邊的關(guān)系。利用Java提供的dom4j技術(shù)解析生成的XML文件，得到模型中狀態(tài)和邊的關(guān)系，并引入圖論的基本原理，采用鄰接表的存儲方式將狀態(tài)和邊的關(guān)系進行存儲，并在每個模型中分別分配給每個狀態(tài)一個編碼，用于簡化模型。為了保證測試用例的完備性，設(shè)計DFS搜