基于概率模型檢驗的cbc通信協(xié)議驗證

基于概率模型檢驗的cbc通信協(xié)議驗證

隨著計算機(jī)網(wǎng)絡(luò)和通信技術(shù)的發(fā)展，基于通信的運(yùn)營權(quán)限（cct）已經(jīng)成為人們研究的重點。cbt系統(tǒng)獨(dú)立于軌道電路。高精度列車定位和多段式高速雙向數(shù)據(jù)的數(shù)據(jù)。它通過駕駛員和基地設(shè)施實現(xiàn)列車控制，這是針對鐵路控制系統(tǒng)的發(fā)展。方向,可滿足鐵路運(yùn)輸智能化、信息化和網(wǎng)絡(luò)化的發(fā)展需要.車地間無線通信是CBTC系統(tǒng)的關(guān)鍵技術(shù)之一.而通信協(xié)議作為車地間無線通信的基礎(chǔ),也是CBTC系統(tǒng)重要的組成部分,它的正確性、穩(wěn)定性和安全性對整個系統(tǒng)有重要影響.傳統(tǒng)的通信協(xié)議驗證方法主要是通過模擬和仿真,可是,模擬和仿真不能保證完全的錯誤覆蓋,同時這兩種方法所消耗的時間也是驚人的.形式化驗證技術(shù)用數(shù)學(xué)的方法驗證一個設(shè)計的功能與性能,能保證對所有的情況進(jìn)行驗證,在系統(tǒng)設(shè)計中得到了廣泛的應(yīng)用.因此,對通信協(xié)議進(jìn)行形式化驗證是很有意義的.CBTC系統(tǒng)車地間無線通信信道具有隨機(jī)特征,因此,CBTC系統(tǒng)的通信子系統(tǒng)亦呈現(xiàn)明顯的統(tǒng)計特征,這導(dǎo)致某些具有隨機(jī)特征的變量以參數(shù)的形式引入到通信協(xié)議中.目前,針對隨機(jī)特征的研究方法主要集中于隨機(jī)Petri網(wǎng)的形式化驗證.可是,由于缺乏時態(tài)邏輯的支持,隨機(jī)Petri網(wǎng)在描述事件發(fā)生的邏輯順序方面存在缺陷,從而限制了隨機(jī)Petri網(wǎng)的應(yīng)用.鑒于此原因,本文作者探討用概率模型檢驗對CBTC系統(tǒng)通信協(xié)議進(jìn)行形式化驗證.概率模型驗證是一種形式化驗證方法,適用于驗證具有隨機(jī)特征的模型.概率模型檢驗采用多端點二叉判決圖(MTBDDs)數(shù)據(jù)結(jié)構(gòu),很好地解決了狀態(tài)空間爆炸問題.同時,概率模型檢驗有時態(tài)邏輯的支持,彌補(bǔ)了隨機(jī)Petri網(wǎng)在描述事件發(fā)生的邏輯順序方面存在的缺陷.本文作者的主要工作是:①綜合了CBTC系統(tǒng)車地通信協(xié)議失效的隨機(jī)錯誤;②設(shè)計了車地安全通信協(xié)議;③建立了通信協(xié)議的概率模型,用概率模型檢驗對其進(jìn)行形式化驗證.1關(guān)于cbt系統(tǒng)的一般介紹CBTC中,車地通信工作分為3個階段:鏈接的建立、維持和釋放.11連接建立只有發(fā)起方有權(quán)主動建立鏈接,跟隨方接收到發(fā)起方的建鏈命令RFC后才能響應(yīng),見圖1(a).22鏈接維護(hù)通信雙方每個周期只進(jìn)行一次數(shù)據(jù)交互.如果應(yīng)用沒有產(chǎn)生任何數(shù)據(jù),通信協(xié)議需要生成心跳信息以維持鏈接,見圖1(b).32連接釋放只有發(fā)起方才能主動釋放鏈接.當(dāng)發(fā)起方不需要鏈接時,向通信協(xié)議下達(dá)釋放鏈接命令,通信協(xié)議主動釋放發(fā)起方的鏈接,見圖1(c).2概率模型試驗2.1馬爾可夫判決過程、連續(xù)時間馬爾可夫鏈模型在概率模型檢驗中,有3類模型:離散時間馬爾可夫鏈(DTMCs),馬爾可夫判決過程(MDPs)及連續(xù)時間馬爾可夫鏈(CTMCs).本文不詳細(xì)介紹3類模型的具體細(xì)節(jié),因為這不是本文工作重點,3類模型的詳細(xì)介紹參見文獻(xiàn).2.2狀態(tài)公式[][]概率模型驗證中,用概率計算樹邏輯PCTL(ProbabilisticComputationalTreeLogic)來刻畫DTMCs和MDPs,用CSL刻畫CTMCs.PCTL是計算樹邏輯CTL的概率性擴(kuò)展,其基本語法如下:?::=true|a|?∧?|??|P??p[ψ]?ψ::=X?|?U≤k?|?U?.?::=true|a|?∧?|??|Ρ??p[ψ]?ψ::=X?|?U≤k?|?U?.這里,需要區(qū)分狀態(tài)公式?和路徑公式ψ,它們分別用來評價狀態(tài)和路徑.a是一個原子命題,??∈{≤,<,≥,>},p∈,k為正整數(shù).時態(tài)運(yùn)算符X(neXt)與U(Until)同傳統(tǒng)的CTL定義一致.X?為真,表示?在當(dāng)前狀態(tài)的下一個狀態(tài)上成立;?1U≤k?2為真,表示存在某一狀態(tài)ω(i)(i≤k),?2在ω(i)上成立,而對于在ω(i)之前的所有狀態(tài),?1都成立;?1U?2為真,表示存在某一狀態(tài)ω(i)(i≥0),?2在狀態(tài)ω(i)上成立,而?1在狀態(tài)ω(i)之前的所有狀態(tài)上都成立.PCTL基本語義如下,對于狀態(tài)s∈S:s|true?對所有s∈S,s|=a?a∈L(s),s|=?1∧?2?s|=?1∧s|=?2,s|=???s|≠?,s|=P??[ψ]?ps(ψ)??p,這里,ps(ψ)=Probs({ω∈Paths|ω|=ψ}).對于路徑ω:ω|=X??ω(1)有意義,并且ω(1)|=?,ω|=?1U≤k?2??i≤k.ω(i)|=?2∧ω(j)|=?1?j<i,ω|=?1U?2??k≥0.ω|=?1U≤k?2.CSL的基本語法和語義與之類似,本文不作詳細(xì)描述,參見參考文獻(xiàn).3環(huán)境狀態(tài)間的信息轉(zhuǎn)移CBTC系統(tǒng)的通信協(xié)議中有3個模塊:發(fā)起方、跟隨方和信道.其中,信道具有典型的隨機(jī)特征.另外,通信協(xié)議數(shù)據(jù)的收發(fā)也伴有隨機(jī)性的延時.根據(jù)通信協(xié)議的原理,圖2中的(a)、(b)和(c)分別抽象出了通信協(xié)議3個模塊的概率模型.對圖2作幾點說明:狀態(tài)間沒有標(biāo)記轉(zhuǎn)移概率的,默認(rèn)其轉(zhuǎn)移概率為1,標(biāo)記轉(zhuǎn)移概率的,其轉(zhuǎn)移概率等于標(biāo)記值.每一個轉(zhuǎn)移都對應(yīng)一系列原子命題及動作,帶有“=”號,或關(guān)系符號“>,>=,<,<=”的,都是原子命題.一個轉(zhuǎn)移中標(biāo)記的所有原子命題為真,則發(fā)生相應(yīng)的狀態(tài)轉(zhuǎn)移.帶有符號“:=”的表示動作,當(dāng)發(fā)生某個狀態(tài)轉(zhuǎn)移時,伴隨著相應(yīng)的動作.比如說,當(dāng)“rack=FALSE&nack>=5*T”為真時,發(fā)起方由狀態(tài)“WAIT-ACK”轉(zhuǎn)移到狀態(tài)“NEW-FRAME”,同時將nack置零.圖2中弧線旁邊標(biāo)注的數(shù)字表示的是狀態(tài)轉(zhuǎn)移的條件,各數(shù)字對應(yīng)的具體條件見表1.圖2中各狀態(tài)及變量含義分別見表2、表3.4pctal的概率規(guī)范本節(jié)用概率模型檢驗工具PRISM對CBTC系統(tǒng)通信協(xié)議進(jìn)行形式化驗證.我們的形式化驗證運(yùn)行在主頻為3.00GHz,內(nèi)存空間為512MB的PC機(jī)中.構(gòu)建模型共耗時0.25s,累計狀態(tài)集合18736個,其中包含一個初始狀態(tài),狀態(tài)轉(zhuǎn)移共計83379個,非確定性選擇共計68038種.我們需要驗證的是CBTC系統(tǒng)通信協(xié)議典型的概率規(guī)范,以期它能達(dá)到期望的性能指標(biāo).對于通信協(xié)議來說,最關(guān)注的莫過于失效率與穩(wěn)定性.由此,總結(jié)出以下典型的概率規(guī)范,并將其轉(zhuǎn)化為PCTL描述的PRISM語言.規(guī)范1:若應(yīng)用軟件不要求釋放鏈接,在不同的信道和系統(tǒng)無故障概率下,通信協(xié)議可以保持鏈接維持狀態(tài)的概率是多少?PRISM語言:Pmax=?[(disconnect=false)U(s=3)&(r=2)];(說明:變量含義與上節(jié)中各狀態(tài)的含義一致;s=0、1、2、3、4分別表示發(fā)起方處于IDLE、NEW-FRAME、WAIT-ACK、DATA、HALT狀態(tài);r=0、1、2、3分別表示跟隨方處于IDLE、RECV-RFC、DATA、HALT狀態(tài),下同)規(guī)范1的驗證結(jié)果如圖3(a).規(guī)范2:發(fā)起方通信中斷的最大概率是多少?PRISM語言:Pmax=?[trueU(s=4)];規(guī)范2的驗證結(jié)果如圖3(b).規(guī)范3:跟隨方通信中斷的最大概率是多少?PRISM語言:Pmax=?[trueU(r=3)];規(guī)范3的驗證結(jié)果如圖3(c).從上述驗證中可以看出,信道正常概率越大且系統(tǒng)無延時概率越大,協(xié)議鏈接維持的概率也越大.定量考慮,從圖3(a)可以看出,當(dāng)p1=0.99,p2=0.99時,協(xié)議鏈接維持概率達(dá)到0.961,已具有一定的穩(wěn)定性,可以作為我們設(shè)計的參考指標(biāo).失效率方面,無論是發(fā)起方還是跟隨方,通信中斷的概率都小于1.5×10-10.根據(jù)CBTC系統(tǒng)通信協(xié)議典型概率規(guī)范的驗證結(jié)果,可以認(rèn)為,我們設(shè)計的通信協(xié)議有比較好的穩(wěn)定性,以及低水平的失效率,具有良好的實用價值.5驗證了系統(tǒng)的穩(wěn)定性本文作者綜合了CBTC系統(tǒng)通信協(xié)議中某些參數(shù)的隨機(jī)特征,用概率模