基于csp理論的多播協(xié)議組合模型

基于csp理論的多播協(xié)議組合模型

1協(xié)議組合技術通信軟件本質上是通信協(xié)議軟件的實現(xiàn)。隨著網(wǎng)絡技術和網(wǎng)絡應用的發(fā)展，通信軟件的功能不斷增強，通信軟件的性能不斷提高。這使得通信協(xié)議變得越來越復雜，通信網(wǎng)絡系統(tǒng)也變得越來越復雜。為了有效管理大型通信網(wǎng)絡系統(tǒng)，降低通信軟件的復雜性，有一種更好的解決方案是采用組件化技術人員。構件化通信軟件的前提是相應的通信協(xié)議必須具有構件化結構.傳統(tǒng)通信協(xié)議,無論是計算機網(wǎng)絡系統(tǒng)中的協(xié)議,還是電信網(wǎng)中的協(xié)議,都采用分層協(xié)議結構,例如開放系統(tǒng)互連(OSI)的7層協(xié)議結構.這種協(xié)議分層結構實際上就是基本的協(xié)議組合結構.這種基本的協(xié)議組合結構,在網(wǎng)絡最初發(fā)展階段,很大程度上解決了網(wǎng)絡系統(tǒng)的復雜性的問題.雖然技術的進步和應用的發(fā)展,單個協(xié)議層內(nèi)的協(xié)議已經(jīng)變得愈來愈復雜,這樣,就需要進一步研究單個協(xié)議層內(nèi)協(xié)議構件化技術.這種協(xié)議構件化技術這就是協(xié)議組合技術,這是一種在20世紀90年代就開始進行研究的協(xié)議設計和驗證.它試圖通過簡單協(xié)議的組合,生成較為復雜的協(xié)議.雖然協(xié)議組合研究這幾年一直都沒有中斷,但是迄今為止協(xié)議組合理論和技術發(fā)展尚不完善,尚未提出較為完整實用的理論模型,也沒有提出實際可用的技術.在最近的網(wǎng)絡協(xié)議國際會議上,還在探討實際組合協(xié)議的驗證問題.目前協(xié)議組合理論和技術研究不完善的主要原因是,沒有建立一個適合于描述協(xié)議組合的協(xié)議理論模型.傳統(tǒng)的協(xié)議模型一般是基于通信有限狀態(tài)機(CFSM)模型,這種模型可以嚴格定義協(xié)議實體內(nèi)部的狀態(tài)變遷與協(xié)議相關事件(例如發(fā)送和接收協(xié)議報文,接收和提交服務原語等),但是,CFSM本身無法描述協(xié)議實體之間的組合運算關系.目前可以查閱到的協(xié)議組合模型都是基于CFSM的協(xié)議組合模型,它們都必須在CFSM之上定義一套組合規(guī)則,而這種組合規(guī)則涉及到許多分布并發(fā)計算理論問題,具有一定的理論難度.所以,就難以保證能夠建立一個簡捷完美的協(xié)議組合的理論模型.協(xié)議組合模型必須基于嚴密的并發(fā)計算理論,這樣,才能有效地解決協(xié)議組合中的同步、并發(fā)等理論問題.以通信順序進程(CSP)這種進程代數(shù)作為理論基礎,定義了一種協(xié)議組合理論模型,并且論證了這種協(xié)議組合模型可以將單播數(shù)據(jù)傳遞協(xié)議組合為多播數(shù)據(jù)傳遞協(xié)議,并且為構件化描述和分析會話發(fā)起協(xié)議(SIP)提供相應的理論基礎.2協(xié)議分層結構模型基于CSP理論的協(xié)議形式化模型是一種面向協(xié)議組合的模型,它包括2個層次的CSP模型:第1個層次是協(xié)議實體模型;第2個層次是協(xié)議交互模型.面向組合的分層協(xié)議模型如圖1所示.這里采用了類似于協(xié)議分層結構中的洋蔥結構,在該結構中只看到某層協(xié)議向上的服務接口,而看不到調(diào)用下層服務的接口.這種洋蔥結構更符合實際面向應用或者面向功能協(xié)議的設計、實現(xiàn)和使用模式.在分層協(xié)議模型中,有關協(xié)議處理的基本機制都在協(xié)議實體這個層次描述.協(xié)議實體層次采用類似于有限狀態(tài)機的“事件觸發(fā)+狀態(tài)變遷”的描述模式,但是,采用CSP描述的一個特點是:主要描述該實體外界可觀察的事件,不描述該實體內(nèi)部不可觀察的行為,例如狀態(tài)變遷等行為.協(xié)議處理的完整機制需要通過多個協(xié)議實體的組合運算描述,主要在協(xié)議交互層描述.這樣,可以根據(jù)不同的需求,分別在不同層次進行相關的協(xié)議建模和描述.2.1csp的信道定義協(xié)議實體模型表示單個協(xié)議實體行為模型.單個協(xié)議實體可以表示為一個CSP的進程表達式,這個進程可以是一個順序進程,也可以是一個由多個順序進程通過組合運算符關聯(lián)的非順序進程.這里協(xié)議實體的進程表達式可以用進程變量PE表示,PE進程表達式的特征可以用四元組(E,C,M,OP)表示.這里E表示該進程的所有事件集合,按照CSP的表示方法,E=αP,這里αP表示進程P的字母表.C表示進程P中的交互連接點集合,這里對CSP中的信道定義進行了一些修改,不采用CSP中的信道的定義,而是采用信道兩個端點的定義,將信道的2個端點稱為交互連接點(connector),也用C表示.采用“連接點”而不是采用“信道”概念的好處在于:可以靈活定義協(xié)議實體之間的交互關聯(lián),定義多個協(xié)議實體交互方式,適合于描述多播模式.M表示進程P與其他進程或者環(huán)境進程交互的報文集合.需要注意的是,報文集合可能與某個交互連接點相互關聯(lián),可能只是限定在某個交互連接點上交互的報文.所以,報文集合中的報文可以攜帶連接點前綴,例如c1.m1表示在連接點c1上的報文m1.OP表示一個CSP運算符的子集.為了簡化協(xié)議進程的描述和驗證,可以選擇一個CSP運算符的子集,作為協(xié)議實體行為表達式的操作運算符.這些操作運算符包括:“!”,在指定連接點發(fā)送一個報文;“?”,在指點連接點接收一個報文,“→”,當某個事件發(fā)生后進入到下一個行為表達式;“|”,具有事件前綴的進程表達式的選擇組合運算符;以及“‖”,2個進程表達式的并發(fā)組合運算符等.2.2連接點關聯(lián)的實現(xiàn)模型按照定義,一個協(xié)議是一組協(xié)議實體之間的交互規(guī)則.所以,協(xié)議的CSP模型就是協(xié)議實體組合的模型.這里協(xié)議的進程可以用進程變量PROT表示,這樣,在CSP理論中,PROT代表的進程表達式的特征可以用五元組(ES,CS,MS,OPS,ENV)表示.ES表示協(xié)議實體集合,也就是該協(xié)議涉及的所有可能的協(xié)議實體類型的集合.這些協(xié)議實體都是具有不同功能或者不同角色的協(xié)議實體,例如協(xié)議發(fā)送實體、協(xié)議接收實體、協(xié)議發(fā)起方實體、協(xié)議響應方實體等.CS表示協(xié)議實體之間交互的連接點關聯(lián)的集合,也就是協(xié)議實體之間交互的連接點的集合的集合.這里連接點之間的關聯(lián)可以涉及兩個以上連接點的關聯(lián),這樣,可以描述多方交互的協(xié)議.這種連接點關聯(lián)的實現(xiàn)模型將在下文做詳細介紹.MS表示在協(xié)議實體連接點關聯(lián)中傳遞的報文集合,這實際上表示的是協(xié)議實體之間傳遞的報文集合,與原來CSP理論中描述的信道上傳遞的報文集合類似.OPS表示在協(xié)議進程表達式中使用的CSP進程組合運算符子集.在協(xié)議模型中主要是協(xié)議實體進程的組合,所以,這里的涉及的CSP運算符主要是進程之間的組合運算符,例如:“□”,進程之間的選擇組合運算符;“;”,進程之間的順序組合運算符等.ENV表示協(xié)議的環(huán)境進程表達式集合.這里可以包括多個進程表達式,例如該協(xié)議用戶實體的進程表達式,該協(xié)議管理實體的進程表達式等.2.3連接點關聯(lián)的csp進程通過定義一個CSP關聯(lián)進程,實現(xiàn)連接點之間的關聯(lián).對于2個連接點之間的關聯(lián),該關聯(lián)進程實現(xiàn)從一個連接點接收報文,然后向另外一個連接點發(fā)送報文.這樣,2個連接點就可以單向關聯(lián).連接點關聯(lián)的CSP進程表達式如下:A(c1,c2)=(c1x→c2!x)對于多個連接點的單向關聯(lián),可以表示為從一個連接點收到報文,然后向其他所有連接點發(fā)送報文.假設被關聯(lián)的連接點集合為C,其中任意一個連接點ci∈C,則連接點集合C的關聯(lián)進程表達式為A(C)=ci:C?x→(‖j≠i(cj!x))這里“‖j≠i(cj!x)”表示向集合C中非ci連接點的所有連接點并發(fā)地發(fā)送報文x.這種連接點關聯(lián)模型,可以在關聯(lián)進程中增加某些網(wǎng)絡對報文處理的行為,便于客觀地描述實際網(wǎng)絡通信環(huán)境.3定義多播傳遞協(xié)議的csp和csp運算G.Singh提出的協(xié)議組合模型也是基于協(xié)議實體的組合模型,2個一對一的數(shù)據(jù)傳送協(xié)議D{i,j}和D{i,k}經(jīng)過組合之后可以生成一對多的數(shù)據(jù)傳送協(xié)議D{i,j,k},但是,這種一對多的數(shù)據(jù)傳送協(xié)議是分別進行多次一對一數(shù)據(jù)傳遞的協(xié)議.這與目前網(wǎng)絡上實際使用的多播協(xié)議處理方式是不同的,也無法達到節(jié)省帶寬資源的目的.下面證明采用以上定義的協(xié)議組合模型可以組合單播數(shù)據(jù)傳遞協(xié)議D{1,2}和D{1,3},得到多播數(shù)據(jù)傳遞協(xié)議D{1,2,3},并且這種多播傳遞協(xié)議只需要發(fā)送方傳遞一次數(shù)據(jù),2個結點都可以接收到數(shù)據(jù).由于定義的協(xié)議組合模型是基于CSP理論的模型,所以以下協(xié)議組合運算完全按照CSP運算規(guī)則進行.這里假定一個從結點1發(fā)送數(shù)據(jù)給結點2的協(xié)議為D{1,2},它包括結點1發(fā)送協(xié)議實體S{1}和結點2的接收實體R{2},2個協(xié)議實體交互連接點分別為c1和c2,則D{1,2}可以表示為:D{1,2}=S{1}‖A(c1,c2)‖R{2},其中,A(c1,c2)=(c1x→c2!x).同理,從結點1向結點3發(fā)送數(shù)據(jù)的協(xié)議D{1,3}可以表示為:D{1,3}=S{1}‖A(c1,c3)‖R{3},其中,A(c1,c3)=(c1x→c3!x).這樣,這兩個協(xié)議組合可以表示為D{1,2}‖D{1,3}=(S{1}‖A(c1,c2)‖R{2})‖(S{1}‖A(c1,c3)‖R{3})通過CSP運算可以簡化為D{1,2}‖D{1,3}=S{1}‖A(c1,c2,c3)‖(R{2}‖R{3})其中,A(c1,c2,c3)=(c1x→(c2!x‖c3!x)).這里的A(c1,c2,c3)完全是現(xiàn)在多播傳遞的模式,即通過連接點c1發(fā)送一次,2個連接點c2和c3都可以收到報文.這說明,定義的協(xié)議組合模型組合出來的協(xié)議完全符合現(xiàn)在網(wǎng)絡協(xié)議的實際模式.這樣,就可以通過協(xié)議組合模型研究多播機制.4sip行為模型的構建SIP協(xié)議分成3個層次,如圖2所示.從上往下包括用戶功能層、事務處理層、報文傳送層.用戶功能層主要為了實現(xiàn)會話創(chuàng)建、修改和終止而進行請求/響應報文的交互,事務處理層主要為了保證請求/響應報文交互的事務處理的完整性而對請求/響應報文的重發(fā)控制,報文傳送層主要根據(jù)請求/響應報文傳輸?shù)囊?分別調(diào)用TCP/UDP/TLS等功能,實現(xiàn)報文的傳遞.圖2SIP協(xié)議實體分層結構及其功能實體劃分實際上,這種協(xié)議實體的劃分還是比較粗糙,無法清楚地表述SIP協(xié)議的交互過程,所以需要進一步分解實體.對于用戶功能層,可以進一步分成為用戶代理客戶端(UAC)、用戶代理服務器(UAS)、有狀態(tài)中介服務器(SFP)、無狀態(tài)中介服務器(SLP),這些實體中的對INVITE請求報文和非INVITE請求報文的處理實體以及對INVITE響應報文和非INVITE響應報文的處理實體,事務處理層可以將其進一步劃分成客戶端事務處理和服務器事務處理.報文傳送層可以進一步劃分成TCP報文傳送實體、UDP報文傳送實體以及TLS報文傳送實體.從圖2可以看出,SIP協(xié)議實體是較為復雜的實體.以下利用協(xié)議組合模型描述一個基本的SIP協(xié)議,說明可以利用協(xié)議組合模型簡化該協(xié)議的描述.如果不考慮中介服務器對請求和響應報文的轉發(fā),SIP協(xié)議的基本行為模型可以表示為僅僅由UAC和UAS組成的交互模型,其UAC和UAS的進程表達式如下.UAC=(GENREQ;CC1;SENDREQ;UAC)□(CHKRESP;CC2;PROCRESP;UAC)UAS=(CHKREQ;CS1;PROCREQ;UAS)□(GENRESP;CS2;SENDRESP;UAS)這里“;”表示進程表達式之間的順序組合運算符;“□”表示進程表達式之間的選擇組合運算符.在UAC的進程表達式中,GENREQ表示在收到SIP用戶服務請求后,將該請求生成請求報文;SENDREQ表示發(fā)送請求報文;CHKRESP表示接收響應報文后者檢查響應報文的正確性及合法性;PROCRESP表示處理響應報文.以上UAC進程代數(shù)表達式表示USC具有兩大類行為:一是接收用戶請求,然后生成和發(fā)送SIP請求報文;二是接收UAS返回的響應,然后處理響應報文,完成一個SIP的請求/響應交互過程.這里的CC1和CC2是連接點關聯(lián)進程,使得順序組合的前后兩個進程能夠交互報文.在UAS的進程表達式中,CHKREQ表示接收到請求報文之后檢查報文的合法性;PROCREQ表示調(diào)用不同進程表達式處理相應的請求報文;GENRESP表示收到SIP用戶的服務響應或者收到請求報文處理過程的指示后生成相應的響應報文;SENDRESP表示發(fā)送響應報文.這里的CS1和CS2也是連接點關聯(lián)進程,使得順序組合前后兩個進程能夠交互報文.同樣,UAS也表示了兩類行為:接收和處理請求報文;生成和發(fā)送響應報文.為了進一步描述UAC和UAS處理過程,需要細化其內(nèi)部進程表達式,例如GENREQ可以細化為如下進程表達式:GENREQ=(GENINVITE□GENCANCEL□GENREGISTER□GENOPTIONS□GENBYE□GENINFO這里,GENINVTTE表示生成INVITE請求報文;GENCANCEL表示生成CANCEL報文;GENREGISTER表示生成REGISTER報文;GENOPTIONS表示生成OPTIONS報文;GENBYE表示生成BYE報文;GENINFO表示生成INFO報文;“□”表示CSP中的進程表達式之間的選擇組合.為了進一步描述具體生成請求報文的行為,需要細化具體報文生成的進程表達式.以下是生成INVITE請求報文的進程表達式:GENINVITE=(sap?InviteReq→setfield(Invite,Request-URI)→serfield(Invite,to)→setfield(Invite,from)→setfield(Invite,Call-ID)→setfield(Invite,CSeq)→setfield(Invite,Max-forwards)→setfield(Invite,Via)→setfield(Invite,Contact)→setfield(Invite,Supported)→setmessagebody(Invite)→c1!Invite→SKIP)這里,sap表示服務訪問點;InviteReq表示從sap接收到的生成INVITE報文請求;setfield表示設置SIP報頭字段的操作事件,其中指定了設置的請求報文Invite以及設置的字段,例如Request-URI.Setmessagebody表示設置報文體的操作事件,其中指定了報文Invite.這里“c1!Invite”表示通過GENINVITE連接點c1發(fā)送已經(jīng)生成的報文Invite.SENDREQ進程可以通過其連接點c2與c1關聯(lián)進程CC1,獲得已經(jīng)生成的Invite報文.這里SKIP表示一個成功結束的進程,這主要是為了滿足CSP中順序組合運算的要求.在完整描述了UAC和UAS行為之后,可以通過組合構成SIP的不同行為特征.例如UAC‖UAS可以表示2個實體的交互協(xié)議,也可以表示2個實體組合的實體.關鍵需要看這些同步組合相關的連接點.這里就需要采用協(xié)議組合模型進行描述.這里假定UAC的服務訪問點為sapc,網(wǎng)絡訪問點為netc,UAS的網(wǎng)