【文章內容簡介】 4% 一般情況 信道帶寬 b比特 /秒，幀長度 l比特，往返傳輸延遲 R秒，則信道利用率為 (l/b) / (l/b + R) = l / (l + Rb) 結論 傳輸延遲大，信道帶寬高，幀短時，信道利用率低。 滑動窗口協議（ 5） 解決辦法 連續(xù)發(fā)送多幀后再等待確認，稱為流水線技術（ pipelining）。 帶來的問題 信道誤碼率高時，對損壞幀和非損壞幀的重傳非常多。 兩種基本方法 退后 n幀（ go back n） 接收方從出錯幀起丟棄所有后繼幀； 接收窗口為 1； 對于出錯率較高的信道，浪費帶寬。 Fig. 315(a) 滑動窗口協議（ 6） 選擇重傳（ selective repeat） 接收窗口大于 1，先暫存出錯幀的后繼幀； 只重傳壞幀； 對最高序號的幀進行確認； 接收窗口較大時，需較大緩沖區(qū)。 Fig. 315(b) 滑動窗口協議（ 7） 退后 n幀協議 協議特點 發(fā)送方有流量控制，為重傳設緩沖； 發(fā)送窗口未滿， EnableNetworkLayer 發(fā)送窗口滿， DisableNetworkLayer 發(fā)送窗口大小 序號個數（ MaxSeq + 1）； 考慮 MaxSeq = 7的情況 1 發(fā)送方發(fā)送 幀 0 ~ 7； 2 序號為 7 的幀的確認被捎帶回發(fā)送方； 3 發(fā)送方發(fā)送另外 8 個幀，序號為 0 ~ 7； 4 另一個對幀 7 的捎帶確認返回。 問題：第二次發(fā)送的 8 個幀成功了還是丟失了？ 退后 n幀重發(fā)； 由于有多個未確認幀，設多個計時器。 滑動窗口協議（ 8） 工作過程 Fig. 316 存在的問題 隱含著信道負載重的假設。若一個方向負載重，另一個方向負載輕，則協議阻塞。 計時器實現 Fig. 317 滑動窗口協議（ 9） 選擇重傳協議（ A Protocol Using Selective Repeat） 目的 在不可靠信道上有效傳輸時，不會因重傳而浪費信道資源，采用選擇重傳技術。 基本原理 發(fā)送窗口大小： MaxSeq，接收窗口大?。?(MaxSeq + 1) / 2 保證接收窗口前移后與原窗口沒有重疊； 設 MaxSeq = 7, 若接收窗口 = 7 發(fā)方發(fā) 幀 0 ~ 6，收方全部收到，接收窗口前移（ 7 ~ 5），確認幀丟失，發(fā)方重傳幀 0，收方作為新幀接收，并對幀 6確認，發(fā)方發(fā)新幀 7 ~ 5，收方已收過幀 0，丟棄新幀 0，協議出錯。 Fig. 319 發(fā)送窗口下界： AckExpected，上界： NextFrameToSend 接收窗口下界： FrameExpected，上界： TooFar 滑動窗口協議（ 10） 緩沖區(qū)設置 發(fā)送方和接收方的緩沖區(qū)大小應等于各自窗口大??； 增加確認計時器，解決兩個方向負載不平衡帶來的阻塞問題； 可隨時發(fā)送否定性確認幀 NAK。 工作過程 Fig. 318 協議說明與驗證（ 1） 協議工程與協議的形式化描述技術 協議工程： 協議說明（ Protocol Specification） 協議驗證（ Protocol Verification） 協議實現（ Protocol Implementation） 協議測試（ Protocol Testing） 一致性測試（ Conformance Testing） 互操作性測試（ Interoperability Testing） 性能測試（ Performance Testing） 協議說明 必須既定義一個協議實體提供給它的用戶的服務，又定義該協議實體的內部操作。 協議說明與驗證（ 2） 協議驗證 驗證協議說明是否完整、正確。 協議實現 用硬件和 /或軟件實現協議說明中規(guī)定的功能。 協議測試 用測試的方法來檢查協議實現是否滿足要求，包括：協議實現是否與協議說明一致（一致性測試）、協議實現之間的互操作能力（互操作性測試）和協議實現的性能（性能測試）等。 在協議的說明、驗證、實現和測試過程中使用形式化描述技術，不僅可以比較容易地理解協議，而且可以使協議描述更加精確，大大簡化了協議的研究工作。 協議說明與驗證（ 3） 形式化描述的意義 實際使用的協議非常復雜，給協議的理解、驗證、實現和測試等工作帶來困難，需要采用形式化的、數學的描述方法來描述協議。但是目前大多數協議還是采用自然語言描述。 自然語言描述協議的缺點 冗余； 多義性； 結構性不好； 不便于自動驗證、測試、實現。 形式化描述技術 FDT（ Formal Description Technique） /形式化方法 FM（ Formal Method）廣泛應用于協議工程研究中 協議說明與驗證（ 4） 一種形式化方法總是以一種形式體系為基礎，只是在具體應用時，大都做了便于描述的改進和擴充。 常用的形式化方法 有限狀態(tài)機 FSM（ Finite State Machine） 擴展： EFSM 形式化語言模型 LOTOS， Estelle， SDL 都有相應擴展 Petri網 擴展：時間 Petri網，隨機 Petri網，高級 Petri網 過程代數（ Process Algebra） 擴展：隨機過程代數 協議說明與驗證（ 5） 有限狀態(tài)機模型 定義 一個有限狀態(tài)機是一個四元組 (S, M, I, T)，其中 S是狀態(tài)的集合； M是標號的集合； I是初始狀態(tài)的集合； T是變遷的集合。 通信協議建模 基本出發(fā)點：認為通信協議主要是由響應多個“事件”的相對簡單的處理過程組成； 事件 命令（來自用戶） 信息到達（來自低層） 內部超時 協議說明與驗證（ 6） 優(yōu)點：簡單明了，比較精確； 缺點：對許多復雜的協議，事件數和狀態(tài)數會劇增，處理困難。 例 協議 3 每個狀態(tài)用三個字母表示： XYZ X：發(fā)送方正發(fā)送的幀序號，為 0或 1； Y：接收方正等待的幀序號，為 0或 1； Z：信道狀態(tài)，為 0， 1， A或 （空）。 初始狀態(tài)為（ 000） 半雙工信道 Fig. 320 全雙工信道 Fig. 321 協議說明與驗證（ 7） 協議驗證 驗證協議說明是否完整正確，以協議說明為基礎，涉及邏輯證明。 主要用于系統(tǒng)實現前的設計階段，為了避免可能出現的設計錯誤。原則上驗證涉及協議所有可能的狀態(tài)。 可達性分析是一種常用的驗證方法 利用圖論知識可以解決狀態(tài)的可達性問題； 可達性分析能夠用來解決協議的不完整性、死鎖和無關變遷等問題。 協議說明與驗證（ 8） Petri網模型 Petri網模型最早在 1962年 Carl