基于CSP的CBTC系統(tǒng)區(qū)域控制器的建模與驗證的開題報告

基于CSP的CBTC系統(tǒng)區(qū)域控制器的建模與驗證的開題報告一、研究背景隨著城市軌道交通的快速發(fā)展，列車間安全距離的保障以及列車運行的可靠性成為各城市軌道交通系統(tǒng)所關(guān)注的問題?；谕ㄐ诺牧熊嚳刂葡到y(tǒng)(CBTC)作為一種先進的列車控制技術(shù)，成為了軌道交通自動化控制領(lǐng)域最熱門的話題之一。CBTC系統(tǒng)的成功運行，引入的是基于通信的區(qū)塊概念代替了固定的軌道電路，在提高系統(tǒng)性能的同時，也為軌道交通系統(tǒng)帶來了新的能力和挑戰(zhàn)。CBTC系統(tǒng)的通信技術(shù)，數(shù)據(jù)傳輸技術(shù)以及運算技術(shù)都非常復(fù)雜，因此系統(tǒng)的開發(fā)和維護需要高度的技術(shù)和嚴謹?shù)姆椒?。CBTC系統(tǒng)主要由車載子系統(tǒng)和地面子系統(tǒng)組成，其中地面子系統(tǒng)通常包括劃分城市地鐵網(wǎng)絡(luò)區(qū)域的控制器和各個子區(qū)域內(nèi)的列車管理系統(tǒng)。為了模擬和檢測CBTC系統(tǒng)的可靠性和性能，需要對系統(tǒng)進行建模和驗證。區(qū)域控制器是CBTC系統(tǒng)的核心部分，其作為各個子系統(tǒng)之間的橋梁，對整個CBTC系統(tǒng)的運行性能和可靠性影響很大，對其建模和驗證具有重要意義。二、研究內(nèi)容本論文旨在開發(fā)基于CSP建模與驗證的CBTC系統(tǒng)區(qū)域控制器建模方法，并基于模型驗證工具驗證其正確性。主要內(nèi)容包括以下方面：1.CBTC系統(tǒng)區(qū)域控制器的建模方法研究與實現(xiàn)。2.基于建模工具驗證模型的正確性，包括模型語義正確性、死鎖和活鎖檢測、驗證組合性質(zhì)等。3.對CBTC系統(tǒng)的成本、效率、可靠性等指標(biāo)進行分析。三、研究意義本論文主要研究基于CSP的CBTC系統(tǒng)區(qū)域控制器建模方法，并將其驗證工具化。主要貢獻如下：1.提出一種基于CSP的CBTC系統(tǒng)區(qū)域控制器建模方案，可應(yīng)用于CBTC系統(tǒng)的其他部分的建模。2.將模型驗證工具運用于CBTC系統(tǒng)區(qū)域控制器的建模與驗證，驗證其正確性和可靠性。3.通過分析CBTC系統(tǒng)的成本、效率、可靠性等指標(biāo)，提供了CBTC系統(tǒng)設(shè)計方面的一些思考和建議。四、研究計劃第一年：1.調(diào)研CBTC系統(tǒng)相關(guān)技術(shù)和研究現(xiàn)狀，分析CBTC系統(tǒng)的結(jié)構(gòu)和運行原理。2.學(xué)習(xí)并掌握CSP建模語言及模型驗證技術(shù)。3.設(shè)計CBTC系統(tǒng)區(qū)域控制器建模方案，完成建模工具的開發(fā)。4.初步運用建模工具驗證建模模型的正確性和可靠性。第二年：1.進行CBTC系統(tǒng)區(qū)域控制器建模和模型驗證，包括死鎖和活鎖檢測、驗證組合性質(zhì)等。2.收集CBTC系統(tǒng)運行數(shù)據(jù)，對系統(tǒng)的成本、效率、可靠性等指標(biāo)進行分析。3.分析CBTC系統(tǒng)的建設(shè)和維護成本，提供設(shè)計建議和性能優(yōu)化方案。第三年：1.完善CBTC系統(tǒng)區(qū)域控制器建模工具，提高驗證效率