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

1、列車自動(dòng)防護(hù)(Automatic Train Protection,簡(jiǎn)稱 ATP)系統(tǒng)是基于通信的列車控制系統(tǒng)的一個(gè)負(fù)責(zé)列車安全的子系統(tǒng)。ATP系統(tǒng)負(fù)責(zé)了列車的測(cè)速、測(cè)距、超速防護(hù)、速度曲線的計(jì)算等等功能。因此,ATP系統(tǒng)軟件的開發(fā)尤為重要。這是列車安全運(yùn)行的保證,目前國內(nèi)對(duì)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,簡(jiǎn)稱UML)是面向?qū)ο箝_發(fā)方法中常用的技術(shù)手段,B方法是一種形式化開發(fā)方法。將B方法與UML語言結(jié)合就能彌補(bǔ)UML語言的不足,結(jié)合之后的方法也具有更精確的語義且無二義性。B方法與傳統(tǒng)的軟件開發(fā)方法一樣,可以參與到從系統(tǒng)需求分析、設(shè)計(jì)到最后系統(tǒng)功能實(shí)現(xiàn)的全過程中去。

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

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