協(xié)議開發(fā)(kāifā)的理論與方法第一頁，共28頁。計(jì)算機(jī)網(wǎng)絡(luò)計(jì)算機(jī)學(xué)科發(fā)展的一個(gè)特征： 應(yīng)用驅(qū)動(dòng)計(jì)算機(jī)網(wǎng)絡(luò)： 應(yīng)用和工程→技術(shù)→科學(xué)理論(lǐlùn)和方法： 體系結(jié)構(gòu)與協(xié)議，協(xié)議開發(fā)第二頁，共28頁。2協(xié)議(xiéyì)研究RoutingQoSMulticastAdmissionControl&CongestionControlSwitchingMiddleware………第三頁，共28頁。3協(xié)議(xiéyì)發(fā)展IBMSNA、ISOOSI/RM和DoDTCP/IP等著名體系結(jié)構(gòu)和協(xié)議已發(fā)揮了不可估量的作用；SNA是協(xié)議體系結(jié)構(gòu)的開拓者；OSI/RM是協(xié)議的指路燈塔；TCP/IP是目前盛行(shèngxíng)的實(shí)事上的工業(yè)標(biāo)準(zhǔn)；XTP、VMTP、Delta-t和NETBLT的出現(xiàn)，將使計(jì)算機(jī)網(wǎng)絡(luò)進(jìn)入一個(gè)高性能的時(shí)代。第四頁，共28頁。4協(xié)議(xiéyì)工程隨著網(wǎng)絡(luò)服務(wù)要求的提高，網(wǎng)絡(luò)系統(tǒng)的復(fù)雜性在協(xié)議(xiéyì)方面體現(xiàn)出空間分布性、并發(fā)性、異步性、不穩(wěn)定性和多樣性，高質(zhì)量的通信協(xié)議(xiéyì)再也不可能靠工程直覺方法來設(shè)計(jì)了；協(xié)議(xiéyì)工程（ProtocolEngineering）用形式化的方法來描述在協(xié)議(xiéyì)設(shè)計(jì)和維護(hù)中的各個(gè)活動(dòng)，建立一套嚴(yán)格的協(xié)議(xiéyì)設(shè)計(jì)方法，使協(xié)議(xiéyì)開發(fā)的整個(gè)過程一體化、系統(tǒng)化和形式化，從而保證協(xié)議(xiéyì)的完整性、正確性、安全性和可移植性。第五頁，共28頁。5協(xié)議(xiéyì)開發(fā)主要活動(dòng)間的關(guān)系第六頁，共28頁。6完整的語法和語義定義；體系結(jié)構(gòu)、服務(wù)和協(xié)議的可表達(dá)性；協(xié)議重要特性的可分析性；支持復(fù)雜協(xié)議的管理；支持逐步求精的方法；支持實(shí)現(xiàn)獨(dú)立性；支持協(xié)議生命期的各環(huán)節(jié)（描述、驗(yàn)證、實(shí)現(xiàn)、一致性測(cè)試(cèshì)、……）；支持自動(dòng)設(shè)計(jì)、驗(yàn)證、實(shí)現(xiàn)和維護(hù)方法。形式(xíngshì)描述技術(shù)FDT的特征第七頁，共28頁。7狀態(tài)變遷模型有限狀態(tài)機(jī)FSM通信(tōngxìn)有限狀態(tài)機(jī)CFSMPetri網(wǎng)程序設(shè)計(jì)語言模型抽象程序CCS，CSP時(shí)態(tài)邏輯FDT種類(zhǒnglèi)第八頁，共28頁。8進(jìn)程代數(shù)（ProcessAlgebra）：用代數(shù)的方法來研究協(xié)議，它有一套完善的等價(jià)理論，如果與網(wǎng)論相結(jié)合，可以用一套完善的分析技術(shù)，提供一個(gè)結(jié)構(gòu)清晰的模型。進(jìn)程代數(shù)與隨機(jī)模型相結(jié)合（如馬爾可夫模型），被應(yīng)用到協(xié)議的性能評(píng)價(jià)(píngjià)?；旌夏Ｐ停ㄈ鐢U(kuò)展的FSM）：擴(kuò)展的FSM過于復(fù)雜并且缺乏形式語義，分析功能較弱。FDT種類(zhǒnglèi)第九頁，共28頁。9國際標(biāo)準(zhǔn)(ɡuójìbiāozhǔn)FDT－SDLSDL(SpecificationandDescriptionLanguage)：FSM+extensions1976年由CCITT(ITU)頒布，一種基于擴(kuò)展?fàn)顟B(tài)變遷和抽象數(shù)據(jù)類型的混合(hùnhé)技術(shù)，被電信公司廣泛用于描述電子分組交換系統(tǒng)，最近已發(fā)布了SDL-2000的新版本。第十頁，共28頁。10國際標(biāo)準(zhǔn)(ɡuójìbiāozhǔn)FDT－LOTOSLOTOS(LanguageOfTemporalOrderingSpecification)：CCS+ADT80年代ISO制訂OSI參考模型時(shí)發(fā)布，1988年確立了最后的國際標(biāo)準(zhǔn)文本。LOTOS提供形式語義，保證描述不存在二義性，便于分析(fēnxī)和一致性測(cè)試?yán)碚摰难芯俊OTOS有二個(gè)組成部分，一部分基于過程代數(shù)，另一部分是基于ACTONE的抽象數(shù)據(jù)類型。第十一頁，共28頁。11FDT的國際標(biāo)準(zhǔn)(ɡuójìbiāozhǔn)－EstelleEstelle(ExtendedStateTransitionModelLanguage)：EFSM+extendedPascalEstelle也是基于擴(kuò)展的狀態(tài)變遷模型(móxíng)，但使用PASCAL語法和數(shù)據(jù)類型，它有一個(gè)形式化的獨(dú)立于實(shí)現(xiàn)的語義。Estelle標(biāo)準(zhǔn)頒布以后，一直到1994年，Estelle研究小組主要致力工具包的研制，1996年以后，Estelle標(biāo)準(zhǔn)又被改進(jìn)了50多處，不過直到現(xiàn)在也沒有見到Estelle的升級(jí)版本。第十二頁，共28頁。12FDT與UML的結(jié)合(jiéhé)近年來UML(UnifiedModelingLanguage)被應(yīng)用到協(xié)議開發(fā)中。UML簡(jiǎn)介UML統(tǒng)一各種面向?qū)ο蠓治龊驮O(shè)計(jì)方法的差異。1995年10月發(fā)布了第一個(gè)版本，現(xiàn)在UML2.0已經(jīng)推出。如今UML已成為一個(gè)流行的、標(biāo)準(zhǔn)化的、通用(tōngyòng)目的面向?qū)ο蟮目梢暬Ｐ驼Z言，許多大的軟件開發(fā)組織開始用它進(jìn)行系統(tǒng)建模。第十三頁，共28頁。13FDT與UML的結(jié)合(jiéhé)UML用于協(xié)議開發(fā)的優(yōu)勢(shì)當(dāng)今的形式化的協(xié)議開發(fā)技術(shù)缺少可視化；不支持協(xié)議開發(fā)的整個(gè)生命周期；而上述兩點(diǎn)正是UML的優(yōu)勢(shì)所在。UML用于協(xié)議開發(fā)的不足UML缺少定義復(fù)雜通信系統(tǒng)協(xié)議的形式化語義，不能直接(zhíjiē)用它來開發(fā)協(xié)議，必須給UML增加一些語義功能。第十四頁，共28頁。14FDT與UML相結(jié)合—BDLBDL(BehaviouralDescriptionLanguage)一個(gè)能夠描述異步并發(fā)行為的語言BDL（把UML的面向?qū)ο蠹夹g(shù)引入到形式化的協(xié)議驗(yàn)證中）；利用BDL可以一致性的操縱包含序列或協(xié)同圖的UML行為視圖，并且不同UML行為視圖可以相互轉(zhuǎn)換；在BDL中，用事件的偏序集合來表示對(duì)象間的相互交互(jiāohù)，用對(duì)象間的一些基本的交互(jiāohù)來描述整個(gè)系統(tǒng)的行為。第十五頁，共28頁。15FDT與UML相結(jié)合—GPDLGPDL(GraphicalProtocolDescriptionLanguage)一個(gè)圖形化的協(xié)議設(shè)計(jì)(shèjì)語言，描述協(xié)議的結(jié)構(gòu)和行為；GPDL的重要性在于把UML的圖形引入到了協(xié)議設(shè)計(jì)(shèjì)中，使之可視化；GPDL包含兩部分：一是圖和文本，圖的結(jié)構(gòu)使協(xié)議設(shè)計(jì)(shèjì)形象化，當(dāng)圖形不能表示時(shí)，就用文字說明；另一部分是GAEL(GenericActionExtensionLanguage)用來表達(dá)協(xié)議的語義信息，以彌補(bǔ)UML的不足。第十六頁，共28頁。16FDT與UML相結(jié)合—GPDLGPDL主要用于協(xié)議(xiéyì)的設(shè)計(jì)和實(shí)現(xiàn)，用GPDL描述的協(xié)議(xiéyì)可以比較容易地轉(zhuǎn)換成SDL標(biāo)準(zhǔn)。

第十七頁，共28頁。17在三種主要的國際標(biāo)準(zhǔn)FDT中，SDL與UML結(jié)合(jiéhé)的是較容易的，因?yàn)镾DL是基于狀態(tài)變遷技術(shù)的，而狀態(tài)圖（statediagram）正是UML建模的5種圖之一；一個(gè)狀態(tài)圖就是一個(gè)狀態(tài)機(jī)；SDL具有抽象數(shù)據(jù)類型，與UML的面向?qū)ο蠹夹g(shù)吻合。SDL-2000第十八頁，共28頁。18SDL-2000SDL-2000是SDL-96和UML技術(shù)(jìshù)有機(jī)結(jié)合的版本，SDL-2000=SDL-96+UML第十九頁，共28頁。19基于(jīyú)Petri網(wǎng)的FDTPetri網(wǎng)理論是在并發(fā)的概念上建立起來的，它直觀地表示了非確定性，可以用于表達(dá)不同抽象級(jí)上的系統(tǒng)概念。Petri網(wǎng)有一套成熟的數(shù)學(xué)理論工具，建立了許多分析技術(shù)，包括可達(dá)性分析、不變量分析(使用線性代數(shù)方法)、保持特性的變換(biànhuàn)(包括化簡(jiǎn))、構(gòu)造理論、形式語言理論、同步距離和網(wǎng)的分解和等價(jià)等。第二十頁，共28頁。20基于(jīyú)Petri網(wǎng)的FDT近幾年人們的注意力集中在如何將代數(shù)的抽象數(shù)據(jù)類型，融合在高級(jí)網(wǎng)結(jié)構(gòu)中，能夠大大地提高描述協(xié)議和服務(wù)所用的高級(jí)Petri網(wǎng)系統(tǒng)(xìtǒng)的表示能力。第二十一頁，共28頁。21基于(jīyú)Petri網(wǎng)的FDT協(xié)議(xiéyì)開發(fā)面臨的挑戰(zhàn)UML用于協(xié)議開發(fā)的優(yōu)勢(shì)自然語言描述的協(xié)議系統(tǒng)到Petri網(wǎng)系統(tǒng)的轉(zhuǎn)換，相應(yīng)的計(jì)算機(jī)輔助工具(gōngjù)的開發(fā)，中間語言、一般模型、轉(zhuǎn)換算法和規(guī)則的建立。第二十六頁，共28頁。協(xié)議(xiéyì)工程（ProtocolEngineering）用形式化的方法來描述在協(xié)議(xiéyì)設(shè)計(jì)和維護(hù)中的各個(gè)活動(dòng)，建立一套嚴(yán)格的協(xié)議(xiéyì)設(shè)計(jì)方法，使協(xié)議(xiéyì)開發(fā)的整個(gè)過程一體化、系統(tǒng)化和形式化，從而保證協(xié)議(xiéyì)的完整性、正確性、安全性和可移植性。三種標(biāo)準(zhǔn)的FDT只支持協(xié)議工程的一至二個(gè)活動(dòng)80年代ISO制訂OSI參考模型時(shí)發(fā)布，1988年確立了最后的國際標(biāo)準(zhǔn)文本。80年代ISO制訂OSI參考模型時(shí)發(fā)布，1988年確立了最后的國際標(biāo)準(zhǔn)文本。支持協(xié)議(xiéyì)工程整個(gè)生命期的FDT？在三種主要的國際標(biāo)準(zhǔn)FDT中，SDL與UML結(jié)合(jiéhé)的是較容易的，因?yàn)橛?jì)算機(jī)學(xué)科發(fā)展的一個(gè)特征：基于(jīyú)Petri網(wǎng)的FDT隨著網(wǎng)絡(luò)服務(wù)要求的提高，網(wǎng)絡(luò)系統(tǒng)的復(fù)雜性在協(xié)議(xiéyì)方面體現(xiàn)出空間分布性、并發(fā)性、異步性、不穩(wěn)定性和多樣性，高質(zhì)量的通信協(xié)議(xiéyì)再也不可能靠工程直覺方法來設(shè)計(jì)了；為適應(yīng)不同規(guī)范及驗(yàn)證的需求，從基本Petri網(wǎng)模型衍化出許多擴(kuò)展模型系統(tǒng)，目前主要有：謂詞/動(dòng)作Petri網(wǎng)、時(shí)間Petri網(wǎng)(TPN)、帶時(shí)態(tài)邏輯的Petri網(wǎng)、顏色Petri網(wǎng)(CPN)、面向?qū)ο驪etri網(wǎng)(OOPN)、隨機(jī)Petri網(wǎng)(SPN)、數(shù)字Petri網(wǎng)(NPN)等。UML用于協(xié)議開發(fā)的優(yōu)勢(shì)基于(jīyú)Petri網(wǎng)的FDT三種標(biāo)準(zhǔn)的FDT只支持協(xié)議工程的一至二個(gè)活動(dòng)Estelle是一種過程語言，可以描述協(xié)議細(xì)節(jié)，用它描述的協(xié)議僅便于實(shí)現(xiàn)；LOTOS描述協(xié)議實(shí)體的外部行為，不關(guān)心實(shí)體內(nèi)部變化，描述的協(xié)議僅便于驗(yàn)證；SDL是一種混合式的FDT，缺乏形式語義，缺乏分析技術(shù)。SDL-2000也只是吸收了UML的一些概念、方法，增加了面向?qū)ο蟮目梢暬O(shè)計(jì)功能，使之更好用，并沒有從本質(zhì)(běnzhì)上提升SDL的分析能力。第二十二頁，共28頁。22基于(jīyú)Petri網(wǎng)的FDTPetri網(wǎng)具有異步特性并發(fā)，決定(juédìng)了它的主要應(yīng)用方向是分布式系統(tǒng)根據(jù)外延公理，變遷的發(fā)生完全由它的外延決定(juédìng)，與系統(tǒng)全局狀態(tài)無關(guān)。因而網(wǎng)系統(tǒng)是異步并發(fā)的“自由王國”，沒有主宰全局的中央控制，這很適合網(wǎng)絡(luò)體系結(jié)構(gòu)、協(xié)議和服務(wù)的特點(diǎn)。第二十三頁，共28頁。23基于(jīyú)Petri網(wǎng)的FDTPetri網(wǎng)的形式基礎(chǔ)使它與其它(qítā)并發(fā)模型建立了連接，這有益于分布式系統(tǒng)的描述和分析。Petri網(wǎng)用直觀的圖形表示形式，與物理系統(tǒng)相近，學(xué)習(xí)和理解這種語言相對(duì)容易。Petri網(wǎng)最大的優(yōu)點(diǎn)是具備一套嚴(yán)密的數(shù)學(xué)理論，各種技術(shù)極有利于驗(yàn)證和分析。第二十四頁，共28頁。24基于(jīyú)Petri網(wǎng)的FDTPetri網(wǎng)表現(xiàn)出面向?qū)ο蠹夹g(shù)的各個(gè)特性，將是一種優(yōu)良的可用圖形(túxíng)表示的面向?qū)ο笳Z言。為適應(yīng)不同規(guī)范及驗(yàn)證的需求，從基本Petri網(wǎng)模型衍化出許多擴(kuò)展模型系統(tǒng)，目前主要有：謂詞/動(dòng)作Petri網(wǎng)、時(shí)間Petri網(wǎng)(TPN)、帶時(shí)態(tài)邏輯的Petri網(wǎng)、顏色Petri網(wǎng)(CPN)、面向?qū)ο驪etri網(wǎng)(OOPN)、隨機(jī)Petri網(wǎng)(SPN)、數(shù)字Petri網(wǎng)(NPN)等。第二十五頁，共28頁。25協(xié)議(xiéyì)開發(fā)面臨的挑戰(zhàn)支持協(xié)議(xiéyì)工程整個(gè)生命期的FDT？協(xié)議(xiéyì)的描述？支持協(xié)議(xiéyì)開發(fā)的工具？第二十六頁，共28頁。26基于Petri網(wǎng)的協(xié)議開發(fā)(kāifā)的問題自然語言描述的協(xié)議系統(tǒng)到Petri網(wǎng)系統(tǒng)的轉(zhuǎn)換，相應(yīng)的計(jì)算