鐵路車站計算機聯(lián)鎖軟件建模研究.pdf

1、鐵路車站計算機聯(lián)鎖系統(tǒng)是運用“故障-安全”技術(shù)、計算機技術(shù)、網(wǎng)絡(luò)技術(shù)以及容錯技術(shù)等實現(xiàn)進路控制功能的系統(tǒng)。它不僅是實時系統(tǒng)，而且是安全-苛求系統(tǒng)。鐵路車站計算機聯(lián)鎖軟件是一種安全苛求軟件，它在保障站內(nèi)的行車安全、行車作業(yè)效率的提升等方面都起到及其關(guān)鍵的作用，是鐵路車站計算機聯(lián)鎖系統(tǒng)的關(guān)鍵組成。
　　目前，對聯(lián)鎖軟件的設(shè)計階段多采用自然語言，表現(xiàn)出很大的歧義性和二義性。本文基于面向?qū)ο罄碚?，綜合采用類圖、用例圖、協(xié)作圖、序列圖、狀態(tài)

2、圖和活動圖對聯(lián)鎖系統(tǒng)的進路控制過程及子過程進行建模?；谛问交椒ǎ捎眯问较到y(tǒng)ALCQI-CTL，對模型進行形式化描述和說明，使模型的歧義性大大降低，減少主觀因素差異造成的設(shè)計錯誤。
　　論文針對車站聯(lián)鎖軟件建模進行研究:
　　(1)給出五元Kripke模型和語義，研究描述邏輯ALCQI，以及其語法和語義描述?；谛问较到y(tǒng)ALCQI-CTL和形式系統(tǒng)ALCQI-CTL的序列圖形式化方法，研究該系統(tǒng)的模型和形式化語義，并對該

3、系統(tǒng)進行可行性分析。
　　(2)建立系統(tǒng)的靜態(tài)模型，研究計算機聯(lián)鎖系統(tǒng)的軟硬件的組成和功能，以基本聯(lián)鎖原理為基礎(chǔ)，采用用例圖對計算機聯(lián)鎖軟件的組成和功能進行描述，并采用類圖設(shè)計信號機、道岔、軌道區(qū)段和進路的數(shù)據(jù)描述以及采用狀態(tài)圖設(shè)計對象的狀態(tài)變化模型。
　　(3)建立系統(tǒng)的動態(tài)模型，基于模塊化思想，并且采用UML的一系列動態(tài)圖建立一次進路控制過程的總體模型和過程的動態(tài)模型。建立一次進路控制過程和子過程的Kripke模型，基于

4、形式系統(tǒng)ALCQI-CTL，并對其進行形式化描述和說明。
　　(4)對模型進行實驗，完成相關(guān)功能的驗證工作。
　　本文的研究結(jié)果表明:綜合采用統(tǒng)一建模語言和形式化方法，能夠高效地消除軟件設(shè)計階段由于人為因素差異造成的的缺陷和錯誤，使得計算機聯(lián)鎖領(lǐng)域?qū)＜液蛙浖_發(fā)人員的聯(lián)系更加緊密，提升聯(lián)鎖軟件的安全性、可靠性;另一方面，能夠在軟件開發(fā)的初始階段就及時發(fā)現(xiàn)軟件設(shè)計中的缺陷和錯誤，同時，也減少了軟件測試和驗證的經(jīng)濟成本。驗證結(jié)果