【正文】 自動加叫： 在被呼叫方正忙的情況下，系統(tǒng)繼續(xù)保持對被呼叫方狀態(tài)的檢測，一旦被呼叫方出現(xiàn)空閑狀態(tài)，則系統(tǒng)將再次對其進行呼叫 。 FSMs ?Many Formal protocol methods are based upon Finite State Machines. ?The ITU Specification and Description Language (SDL) is one such formal specification method ?Most protocols defined by ITU after the advent of SDL are described using SDL. ?Prior to the introduction of SDL protocols were described using a variety of different methods including natural language. 第 3章 協(xié)議形式化描述技術 (1－概述及 FSM) 86 Protocol Specification amp。 Synchronous Communication ? There are two approaches to implementing message passing: Synchronous amp。 當前狀態(tài) 協(xié)議動作 輸出狀態(tài) q0 輸入 x, y q1 q1 x y q2 q1 x y q3 q1 x = y q4 q2 x = x – y q1 q3 y = y – x q1 q4 輸出 x q5 q5 將狀態(tài)變遷條件 (謂詞 )、變量賦值和 I/O操作放在同一列，統(tǒng)一用協(xié)議動作 (Action)來表示。過程一開始處于初始狀態(tài) q0，等待輸入變量 x和 y的值。 ?還可以減少 FSM的狀態(tài)空間。集合中的值可以是變量表達式或者是常量數(shù)值。 ?可以用有限狀態(tài)機來描述一個具有有限取值范圍的變量。 ?變量與隊列的主要區(qū)別是變量一次只能保存一個值，可以將變量取值范圍內(nèi)的任意值賦給該變量，但是我們只能獲取最后一次賦給變量的值。 ?可以從三個方面對前述基本的 FSM進行擴展： ?變量； ?用傳送整型值的隊列來代替?zhèn)魉臀炊x數(shù)據(jù)類型的抽象數(shù)據(jù)對象隊列； ?引入一組操縱變量的算術和邏輯操作符。 第 3章 協(xié)議形式化描述技術 (1－概述及 FSM) 51 停止等待協(xié)議： Summary ?當描述比較復雜的協(xié)議時，狀態(tài)的數(shù)目將急劇增加，以致很難用它來清晰地描述協(xié)議。從理論上講，應當共有 2?2?4 = 16種不同的狀態(tài)。最終，發(fā)送過程超時 (轉(zhuǎn)換 7)，且系統(tǒng)回到狀態(tài) (000)。在無差錯的情況下，系統(tǒng)的狀態(tài)僅在 4個狀態(tài)中循環(huán)：(000)→ (01A)→ (111)→ (10A)→ (000)→ … 。 第 3章 協(xié)議形式化描述技術 (1－概述及 FSM) 50 停止等待協(xié)議：合并后的狀態(tài)變遷圖 變遷 意義 0 幀丟失或幀出錯 1 收 [0]，發(fā) ACK，送主機 2 收 ACK，發(fā) [1] 3 收 [1]，發(fā) ACK，送主機 4 收 ACK，發(fā) [0] 5 收 [0]，發(fā) ACK，不送主機 6 收 [1]，發(fā) ACK，不送主機 7 超時，發(fā) [0] 8 超時，發(fā) [1] 0 0 0 0 0 0 1 2 3 4 5 6 7 8 8 7 0 0 0 0 1 0 1 1 1 1 0 1 1 0 ? 1 1 ? 0 1 ? 0 0 ? 1 0 A 0 1 A 假設系統(tǒng)一開始處在 (000)狀態(tài)。 ?整個系統(tǒng)的狀態(tài)是通信雙方兩個協(xié)議機和信道的所有狀態(tài)的組合。 ?解決辦法：合并一些狀態(tài) ,即考慮一些次要的細節(jié) 第 3章 協(xié)議形式化描述技術 (1－概述及 FSM) 49 停止等待協(xié)議：狀態(tài)變遷圖合并 ?狀態(tài)合并： ?甲方的狀態(tài) 1和狀態(tài) 2，狀態(tài) 3和狀態(tài) 4都可以合并， ?乙的狀態(tài) 1和狀態(tài) 4，狀態(tài) 2和狀態(tài) 3也可進行合并。 Why? ?甲方和乙方的狀態(tài)各有 4個， ?而信道上的狀態(tài)也有 4個 (即：信道上傳送 [0]，傳送 [1]，傳送 ACK，以及出現(xiàn)差錯或幀的丟失 )。如合在一起用一個有限狀態(tài)機來描述整個系統(tǒng)，將會更加清楚。但這里就將 “ 收 [0]”與 “ 發(fā)ACK”合并成為一個事件。但這里就將 “ 收 [1]”與“ 發(fā) ACK”合并成為一個事件。 第 3章 協(xié)議形式化描述技術 (1－概述及 FSM) 46 停止等待協(xié)議：狀態(tài)變遷表 第 3章 協(xié)議形式化描述技術 (1－概述及 FSM) 47 停止等待協(xié)議：狀態(tài)變遷圖 1 2 3 4 1 2 3 4 等待 準備發(fā) ACK 準備發(fā) ACK 準備發(fā) [0] 準備發(fā) [1] 期望收 [1] 期望收 [0] 等待 發(fā) [0] 發(fā) [1] 收 [1] 收 [0] 發(fā) ACK 發(fā) ACK 收 ACK 收 ACK 發(fā) ACK 收 [1] 發(fā) ACK 收 [0] 甲方 乙方 超 時 超 時 狀態(tài)符號 狀態(tài)編號 狀態(tài)含義 狀態(tài)變遷 輸入事件 對某些狀態(tài)進行了簡化。 ?當收到無差錯的幀但序號不正確時，要發(fā)確認幀，同時要丟棄此幀，不送主機。 ?將 0號幀和 1號幀分別記為 [0]和 [1]。例如： ?對于輸入串 {a0, a1, …, a n1}，設： ? ?(s0 , a1) = s1, ? ?(s1 , a2) = s2, …. ? ?(sn1 , an1) = sn ?這時輸出序列為： ?(s0, a0) ?(s1 , a1) … ?(sn1 , an1) 第 3章 協(xié)議形式化描述技術 (1－概述及 FSM) 44 Mealy 機 vs. Moore機 ? Moore機可看做是 Mealy機的一個特例， Why? ?對于任何一個 Moore機 M = (S, s0, I, O, ?, ?) : ?設當輸入串為 {a0, a1, …, a n1}時，其輸出序列為： ?(s0) ?(s1) … ?(sn)，其中 si 和 ai1 滿足： ?(si1, ai1) = si， 1? i ?n ?引入： S ? I 到 O的映射 ??： ? ??(si1, ai1) = ?{?(si1, ai1)} = ? (si), 1? i ?n ?這樣得到一個 Mealy機 M?= (S, s0, I, O, ?, ??)，對于輸入串 {a0, a1, …, a n1}， Mealy機 M?的輸出為 ??為： ??(s0, a0) ??(s1, a1)… ??(sn1, an1) = ?(s0) ?(s1) … ?(sn1) 第 3章 協(xié)議形式化描述技術 (1－概述及 FSM) 45 Mealy機： Example ?停止等待協(xié)議： ?設甲、乙雙方進行半雙工通信，甲發(fā)信息幀，乙回送確認幀。在這里規(guī)定， s = ?(s , ?)， 即對任何狀態(tài) s，當讀入空字符 ?時，有很狀態(tài)機不發(fā)生任何狀態(tài)轉(zhuǎn)移。 ?? ： S ? I ? 2S是狀態(tài)轉(zhuǎn)換函數(shù)，如果在某一確定的時刻， FSM處于某一狀態(tài) si ? S, 并接收一個輸入字符 aj? I，那么下一時刻將處于一個確定的狀態(tài) s180。在任一確定的時刻， FSM只能接收一個確定的輸入 aj。在任一確定時刻，F(xiàn)SM只能處于一個確定的狀態(tài) si。例如： ?對于輸入串 {a0, a1, …, a n1}，設： ? ?(s0 , a0) = s1, ? ?(s1 , a1) = s2, …. ? ?(sn1 , an1) = sn ?這時輸出序列為： ?(s0) ?(s1) … ?(sn1) 第 3章 協(xié)議形式化描述技術 (1－概述及 FSM) 40 Moore 機 vs. 有限狀態(tài)機 ?有限狀態(tài)機可看做是 Moore機的一個特例， Why? ?對于任何一個有限狀態(tài)機 M = (S, s0, I, ?, F): ?引入輸出字符集合 O = {0, 1}，并定義 S到 O的映射 ? 為： ?對于 s ? F, ?(s) = 1；對于 s ? F, ?(s) = 0 ?這樣得到一個 Moore機 M?= (S, s0, I, O, ?, ?)，在該 Moore機中，輸出為 1的狀態(tài)為終結狀態(tài)，輸出為 0的狀態(tài)即為非終結狀態(tài)。在這里規(guī)定， s = ?(s , ?)， 即對任何狀態(tài) s，當讀入空字符 ?時，有很狀態(tài)機不發(fā)生任何狀態(tài)轉(zhuǎn)移。 ?? ： S ? I ? 2S是狀態(tài)轉(zhuǎn)換函數(shù)，如果在某一確定的時刻， FSM處于某一狀態(tài) si ? S, 并接收一個輸入字符 aj? I，那么下一時刻將處于一個確定的狀態(tài) s180。在任一確定的時刻， FSM只能接收一個確定的輸入 aj。在任一確定時刻，F(xiàn)SM只能處于一個確定的狀態(tài) si。 ?實際上生活中的許多有限狀態(tài)系統(tǒng)對于不同的輸入信號，除內(nèi)部狀態(tài)不斷改變外，還不斷向系統(tǒng)外部輸出各種信號。這時可用如下兩種方式來表示 FSM： ?FSM = (S, I, ?)或 ?FSM = (S, s0, I, ?) 第 3章 協(xié)議形式化描述技術 (1－概述及 FSM) 24 Finite State Machines (FSMs) 三、 Representation 第 3章 協(xié)議形式化描述技術 (1－概述及 FSM) 25 State Transition Diagrams ?Used to Visually represent an FSM ?Emphasis is on identifying states and possible transitions ?Circles represent States ?Arrows represent Transitions ?ei are inputs ?xi are outputs S1 S2 e1/x1 e1/x2 e2/x4 e2/x3 第 3章 協(xié)議形式化描述技術 (1－概述及 FSM) 26 FSM Tables (狀態(tài)轉(zhuǎn)換表 ) ? All inputs, states, state transitions and outputs of a FSM can be listed in a Table format input events outputs current state next state S1 S2 S1 S2 x1 x2 x3 x4 S2 e1 e1 e2 e2 S2 S1 S1 ? Each row of the table is one unique bination of Input Events and Current State ? For plete definition of FSM all Event/State binations shall be provided ? Table is another way to represent an FSM with an emphasis on exploring all Event/State binations 第 3章 協(xié)議形式化描述技術 (1－概述及 FSM) 27 FSM Table Compact Form ? Here in the top row of the Table has a list of all States while first column has a list of all Input Event. ? Table Field on the intersection represents the transition function for the State, Event bination ? Each field conta