協(xié)議開發(fā)的理論與方法(完整版)
【正文】 需 求服 務(wù) 描 述體 系 結(jié) 構(gòu) 設(shè) 計(jì)協(xié) 議 描 述目 標(biāo) 實(shí) 現(xiàn)構(gòu) 造定 義 服 務(wù)協(xié) 議 綜 合自 動 實(shí) 現(xiàn)驗(yàn) 證一 致 性 測 試性 能 分 析7 ? 完整的語法和語義定義； ? 體系結(jié)構(gòu) 、 服務(wù)和協(xié)議的可表達(dá)性； ? 協(xié)議重要特性的可分析性； ? 支持復(fù)雜協(xié)議的管理； ? 支持逐步求精的方法； ? 支持實(shí)現(xiàn)獨(dú)立性； ? 支持協(xié)議生命期的各環(huán)節(jié) （ 描述 、 驗(yàn)證 、實(shí)現(xiàn) 、 一致性測試 、 …… ） ； ? 支持自動設(shè)計(jì) 、 驗(yàn)證 、 實(shí)現(xiàn)和維護(hù)方法 。 形式描述技術(shù) FDT的特征 8 ? 狀態(tài)變遷模型 ? 有限狀態(tài)機(jī) FSM ? 通信有限狀態(tài)機(jī) CFSM ? Petri網(wǎng) ? 程序設(shè)計(jì)語言模型 ? 抽象程序 ? CCS， CSP ? 時態(tài)邏輯 FDT種類 9 ? 進(jìn)程代數(shù) （ Process Algebra） ：用代數(shù)的方法來研究協(xié)議 ， 它有一套完善的等價理論 ， 如果與網(wǎng)論相結(jié)合 ， 可以用一套完善的分析技術(shù) ， 提供一個結(jié)構(gòu)清晰的模型 。 ? Estelle標(biāo)準(zhǔn)頒布以后 ， 一直到 1994年 ， Estelle研究小組主要致力工具包的研制 ， 1996年以后 ， Estelle標(biāo)準(zhǔn)又被改進(jìn)了 50多處 ， 不過直到現(xiàn)在也沒有見到 Estelle 的升級版本 。 16 FDT與 UML相結(jié)合 —GPDL ? GPDL (Graphical Protocol Description Language ) ? 一個圖形化的協(xié)議設(shè)計(jì)語言 ， 描述協(xié)議的結(jié)構(gòu)和行為； ? GPDL的重要性在于把 UML的圖形引入到了協(xié)議設(shè)計(jì)中 ， 使之可視化； ? GPDL包含兩部分：一是 圖 和 文本 ， 圖的結(jié)構(gòu)使協(xié)議設(shè)計(jì)形象化 ， 當(dāng)圖形不能表示時 ， 就用文字說明；另一部分是 GAEL (Generic Action Extension Language)用來表達(dá)協(xié)議的語義信息 ， 以彌補(bǔ) UML的不足 。 23 基于 Petri網(wǎng)的 FDT ? Petri網(wǎng)具有異步特性并發(fā) ， 決定了它的主要應(yīng)用方向是分布式系統(tǒng) 根據(jù)外延公理 ， 變遷的發(fā)生完全由它的外延決定 ， 與系統(tǒng)全局狀態(tài)無關(guān) 。 ? 協(xié)議 Petri網(wǎng)描述到協(xié)議實(shí)現(xiàn)的自動化，建立Petri網(wǎng)編譯系統(tǒng)，實(shí)現(xiàn)網(wǎng)系統(tǒng)
教學(xué)課件相關(guān)推薦
鄂ICP備17016276號-1