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

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

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