ATP系統(tǒng)形式化開發(fā)方法的研究.pdf

1、列車自動防護(hù)(Automatic Train Protection,簡稱 ATP)系統(tǒng)是基于通信的列車控制系統(tǒng)的一個負(fù)責(zé)列車安全的子系統(tǒng)。ATP系統(tǒng)負(fù)責(zé)了列車的測速、測距、超速防護(hù)、速度曲線的計算等等功能。因此,ATP系統(tǒng)軟件的開發(fā)尤為重要。這是列車安全運行的保證,目前國內(nèi)對ATP系統(tǒng)的研究成果還不是很成熟,然而ATP系統(tǒng)的系統(tǒng)化和網(wǎng)絡(luò)化程度非常的高,且非常龐大和復(fù)雜,采用形式化方法建立其系統(tǒng)的整體模型能夠更為直觀的理解和分析車載 AT

2、P系統(tǒng),并可以消除軟件開發(fā)的二義性,減小軟件開發(fā)成本,保證ATP系統(tǒng)功能的邏輯正確性和完備性。
　　統(tǒng)一建模語言(Unified Modeling Language,簡稱UML)是面向?qū)ο箝_發(fā)方法中常用的技術(shù)手段,B方法是一種形式化開發(fā)方法。將B方法與UML語言結(jié)合就能彌補UML語言的不足,結(jié)合之后的方法也具有更精確的語義且無二義性。B方法與傳統(tǒng)的軟件開發(fā)方法一樣,可以參與到從系統(tǒng)需求分析、設(shè)計到最后系統(tǒng)功能實現(xiàn)的全過程中去。

3、r>　　本文以列車ATP系統(tǒng)為研究對象,圍繞著對ATP系統(tǒng)建模和驗證方法展開研究。選取UML靜態(tài)模型圖中的類圖和狀態(tài)圖,采用B方法的抽象機語言對UML類圖和狀態(tài)圖進(jìn)行形式化描述,建立了類圖和狀態(tài)圖到 B方法抽象機之間的映射關(guān)系。最后將UML類圖和狀態(tài)圖到B方法的形式化規(guī)約應(yīng)用到ATP系統(tǒng)的列車間距控制功能、車門控制功能、超速防護(hù)功能上去,應(yīng)用proB作為模型驗證工具,驗證了ATP系統(tǒng)功能的模型正確性。
　　本論文通過形式化建模和其

4、驗證方法,改進(jìn)了目前 ATP系統(tǒng)需求規(guī)范的建模和驗證方法。與傳統(tǒng)的建模和驗證方式只能簡單應(yīng)用到 ATP系統(tǒng)的某一個功能不同,這個方法能用到整個ATP系統(tǒng)中去。
　　針對ATP系統(tǒng)的特點,通過UML類圖和狀態(tài)圖到B方法形式化規(guī)約的映射關(guān)系,將形式化方法應(yīng)用于ATP系統(tǒng)建模和驗證的過程中去,強化了ATP系統(tǒng)建模和驗證的安全。并且應(yīng)用proB作為模型驗證工具,不會像其他B方法開發(fā)工具那樣猜測操作參數(shù)的正確性,從而使模型驗證結(jié)果更為準(zhǔn)確。