1、網絡協議工程網絡協議工程南京郵電大學計算機學院2/89第第3 3章章 協議模型技術協議模型技術3.1 3.1 引言引言3.2 3.2 有限狀態機有限狀態機(fsm)(fsm)3.3 petri3.3 petri網網3.4 3.4 時序邏輯時序邏輯(tl)(tl)3.5 3.5 通信進程演算通信進程演算(ccs)(ccs)3/893.1 3.1 引言引言協議模型技術是協議工程的核心技術之一，是協議工程的基礎。形式描述語言、協議正確性驗證、協議自動化實現以及協議測試都基于某種模型技術。協議模型技術旨在精確地表述(n-1)層通道，n層局部系統和全局系統的行為和性質。n層局部系統由各種協議元素組成，因

2、此，模型技術必須精確地表述各種協議元素的性質和行為，以及它們之間作用關系(即協議機制)。全局系統性質即協議性質。4/893.1.1 3.1.1 協議性質協議性質3.1.1 3.1.1 協議性質協議性質3.1.2 3.1.2 協議元素性質協議元素性質3.1.3 3.1.3 通道類別通道類別3.1.4 3.1.4 協議模型的選取協議模型的選取5/893.1.1 3.1.1 協議性質協議性質一個好協議應該具有的協議性質，主要包括：1 活動性(liveness)2 安全性(safety)3 一致性(consistency)4 完備性(completeness)6/893.1.1 3.1.1 協議性質協

3、議性質1 活動性協議活動性指協議運行時發生所期望的事情，包括：預定的事件會產生、指定的協議狀態會達到、應該進行的協議行動會進行等等。活動性體現在終止性和進展性兩個方面，如果協議有終止性和進展性也就具有活動性。終止性協議從任何一個狀態開始運行，總能正確地達到終止狀態。進展性協議從初始狀態運行，總能正確地達到指定狀態。某些情況下，終止狀態和初始狀態是同一的，協議從初始狀態開始運行總能正確地回到初始狀態，并可反復運行，即具有回歸性。回歸性終止性進展性活動性7/893.1.1 3.1.1 協議性質協議性質活動性可以從事件狀態表觀察和分析協議活動性。一個簡單系統示例：s0s1s2s3i1o1s1o3s3

4、i2o2s2o3s3i3s0s0s0(a) 事件狀態表(b) fsm圖8/893.1.1 3.1.1 協議性質協議性質2 安全性(safety)協議安全性指協議運行時沒有壞事情出現。這些壞事情包括不可接收的事件、不可進一步向前的狀態、錯誤的行動、錯誤的條件、變量值越界等等。壞事情一般導致兩種現象：死鎖(deadlock)協議堵塞在某一個狀態而無法向前活鎖(livelock)協議作無意義的循環示例：從事件狀態表和fsm觀察死鎖和活鎖現象。假定o1-i2不能保證，即不能產生i2(壞事情產生)，則系統在s0時收到i1之后就永遠停止在s1上，除非再次輸入i3，否則無法回到s0，即死鎖。假定s3收到i3

5、后，輸出o2,轉到s0，則導致s0、s1和s3無止境循環，即活鎖。9/893.1.1 3.1.1 協議性質協議性質3 一致性一致性是指協議服務行為(性質)和協議行為(性質)一致。一致性包括兩個方面：協議應該提供用戶要求的服務；協議無需提供用戶沒有要求的服務。10/893.1.1 3.1.1 協議性質協議性質4 完備性完備性是指協議性質完全符合協議環境的各種要求，即協議的構造考慮了用戶要求、用戶特點、通道性質、工作模式等各種潛在因素的影響，考慮了各種錯誤事件、異常情況的處理。11/893.1.1 3.1.1 協議性質協議性質注1：協議性質的分類一般性質：與協議具體內容無關的性質，如：安全性和活動

6、性。協議驗證技術所側重的。特殊性質：與協議具體內容相關的性質，如：一致性和完備性協議測試技術所側重的。注2：一致性部分正確性等價性完備性完全正確性有界性：協議元素性質和通道性質12/893.1.2 3.1.2 協議元素性質協議元素性質協議元素性質對協議模型有重要影響協議元素性質如下：1 事件成對性2 事件原子性3 事件時序性4 狀態時序性5 變量有界性6 過程的原子性13/893.1.2 3.1.2 協議元素性質協議元素性質事件成對性事件分通信事件和內部事件兩類，通信事件是成對出現的，而內部事件不是成對出現的。例如，n層用戶發出服務原語(輸出事件)和n層協議接收到服務原語(輸入事件)成對地出現

7、在(n)sap的兩側， (n)sap為事件發生點。n層協議實體a發出一個pdu和b收到一個pdu是一對通信事件，出現在兩個(n-1)sap上，出現在兩個不同的事件發生點。14/893.1.2 3.1.2 協議元素性質協議元素性質事件成對性通信事件分兩類：同步事件(也叫協同事件)：輸入事件和輸出事件發生在同一個事件點上，同時出現。異步事件：輸入事件和輸出事件發生在兩個事件點上，不同時出現，輸出事件滯后于輸入事件15/893.1.2 3.1.2 協議元素性質協議元素性質事件原子性不論通信事件還是內部事件要么不發生，一旦發生就一定完成，這種性質稱為事件的原子性。有原子性的事件稱為原子事件(atomi

8、c events)。例如，當n層協議實體向(n-1)層通道輸出一個報文時，輸出一旦啟動，即使是輸出失敗(通道丟失報文)，事件“輸出報文”也認為已發生。假定所有事件都有原子性。16/893.1.2 3.1.2 協議元素性質協議元素性質事件時序性服務原語狀態圖表述了服務原語的時序關系pdu交換規則表述了pdu的時序關系通信事件由服務原語和pdu的交換引起，因此，服務原語狀態圖和pdu交換規則決定了通信事件時序性。狀態時序性事件時序性決定了狀態時序性變量有界性協議變量的取值范圍有明確定義17/893.1.2 3.1.2 協議元素性質協議元素性質過程的原子性一個協議過程可能包括多個協議行動，過程一旦啟

9、動之后，所有包括的行動一次性完成，不經歷中間協議狀態，不被其它過程打斷，這種性質就是過程的原子性，具有原子性的過程為原子過程。協議運行時，從一個狀態到另一個狀態的轉換可處理成原子過程。18/893.1.3 3.1.3 通道類別通道類別通道分成三類：空通道報文的傳送時間和延時時間為0的通道。非緩沖通道任何時刻，最多只有一個正在傳送中報文的通道緩沖通道允許有多個報文停留的通道19/893.1.3 3.1.3 通道類別通道類別事件點、事件通道的兩端為兩個通信事件發生點，一個報文從通道一端傳送到另一端的過程中，兩個事件點產生四個事件。兩個端點分別標記為a和b，假定報文從a端傳送到b端，經歷：a端用戶通

10、道a端通道b端b端用戶四個事件的含義：a!m a端用戶向通道a端發送報文ma?m 通道從a端接收報文m，并啟動傳送b!m 通道完成報文傳送，將報文發送給b端用戶b?m b端用戶從通道b端接收報文20/893.1.3 3.1.3 通道類別通道類別四個事件的含義：a!m a端用戶向通道a端發送報文ma?m 通道從a端接收報文m，并啟動傳送b!m 通道完成報文傳送，將報文發送給b端用戶b?m b端用戶從通道b端接收報文a!m與a?m 、b!m與b?m是協同事件(同步事件)a!m與b?m 、a?m與b!m是異步事件假設報文傳送延時t秒，異步事件延遲為t秒對于空通道，t0， a!m與b?m 、a?m與b

11、!m可處理為同步事件。通道工作方式可以是單工、半雙工、全雙工。全雙工可視為兩個獨立的單工通道。21/893.1.4 3.1.4 協議模型的選取協議模型的選取來自數學模型(或方法)、自動機模型(或程序模型)理想的協議模型能方便地充分地表示協議元素和通道的各種性質，有強的表達能力和實用性；容易觀察協議性質，容易進行協議驗證和測試。模型fsm、petri網等22/893.2 3.2 有限狀態機有限狀態機(fsm)(fsm)fsm定義通道fsm協議實體fsmfsm簡化fsm合成fsm擴充23/893.2.1 fsm定義有限狀態機fsm定義為四元系統，其中，s是系統狀態集，狀態數有限，(無限狀態機為圖靈

12、機)i為系統初始狀態，ise為原子事件集t為狀態轉換函數集24/893.2.1 fsm定義有限狀態機fsm轉換函數定義為當系統處于狀態si時，如果發生事件e，那么系統狀態變成sj。fsm可以用于協議模型技術能表示協議元素的時序性以及狀態隨事件變化的關系具有直觀易懂的優點。eesssstssjijei,25/893.2.1 fsm定義有限狀態機fsm圖形表示法圓圈 表示狀態，圓圈內的符號表示狀態含義弧 帶箭頭的弧表示狀態轉換，弧的標識表示事件黑點圓 中心為黑點的圓表示初始狀態方框 表示系統邊界， 邊框上的小圓表示事件發生點(或系統和外界的耦合點)。26/893.2.2 通道fsm空通道狀態數為1

13、，即只有一個初始狀態。真正的空通道不存在，但是我們有時可將非緩沖通道簡化成空通道。非緩沖通道假設一個方向上傳送的報文相同，則單工非緩沖通道狀態數為2，半雙工的狀態數為3，全雙工的狀態數為4。27/893.2.2 通道fsm非緩沖通道fsm示例：28/893.2.2 通道fsm圖(a)表示單工fsm，初始狀態表示通道中無報文，狀態1表示報文在傳送中，ma表示a端用戶報文。圖(c)表示半雙工fsm,狀態1表示a端用戶報文ma在傳送中，狀態2表示b端用戶報文mb在傳送中。29/893.2.2 通道fsm緩沖通道其狀態數隨通道中允許停留的報文數目和報文種類數而急劇增加。如果所有報文相同，則隊列邊界為n

14、的單工緩沖通道的狀態數為(n+1)，隊列邊界表示通道中緩沖隊列的最大允許長度；對于全雙工通道，狀態數為(n+1)2很多情況下，通道中的報文是不同的，如，順序號不同。如果通道中有多個不同的報文(每種報文最多一個，并且報文有序)，那么邊界為n的單工緩沖通道的狀態數為2n個。30/893.2.2 通道fsm緩沖通道31/893.2.3 協議實體fsm以ab協議系統為實例，說明怎樣用fsm表示協議實體32/893.2.3 協議實體fsm圖(a)為ab協議系統，s和r為協議實體，s表示發送端，r表示接收端。a、b分別為ab協議系統和其用戶的耦合點。通道ch為非緩沖通道，端點分別為a和b。33/893.2

15、.3 協議實體fsms有四個狀態1 s已從a接收報文，順序號置成0，報文命名為m02 s已向a發出m0，等待r的ack03 s已從a接收報文，順序號置成1，報文命名為m14 s已向a發出m1，等待r的ack1r有四個狀態1 r已從b接收報文m02 r已向b發ack03 r已從b接收報文m14 r已向b發ack134/893.2.3 協議實體fsm圖(b)為s的fsm圖(c)為r的fsm35/893.2.4 fsm簡化fsm的缺點是會產生狀態爆炸。隊列邊界為n的系統的fsm的狀態數可大于2n，兩個狀態數為x和y的fsm合并后的狀態數可為xy。fsm簡化旨在減少狀態數。36/893.2.4 fsm

16、簡化fsm簡化方法方法1 狀態層次化方法2 使用原子過程方法3 使用協議變量方法4 隱藏內部協同事件方法5 通道fsm的簡化37/893.2.4 fsm簡化方法1 狀態層次化將若干協議功能按階段組織起來設置狀態，然后分階段設立子狀態，可大大減少每一級的狀態數。如：iso t層協議設立22個總狀態，數據傳輸階段為狀態open，在此階段還包括若干子狀態。在只考慮連接建立和撤銷等協議功能時，定義22個總狀態就可以了。如：tcp協議設立了12個總狀態。數據傳輸階段為狀態estab。38/893.2.4 fsm簡化方法2 使用原子過程在fsm的四元系統中，如果轉換函數sisjt和sjskt能夠合并成si

17、skt，那么狀態sj就可以消去。兩個轉換函數對應于兩個協議過程，它們能夠合并的準則是：合并后的過程為原子過程。如：單工非緩沖通道的a?ma和b!ma, a?ma和drop可合并成兩個原子過程。39/893.2.4 fsm簡化方法3 使用協議變量fsm擴充中使用該方法40/893.2.4 fsm簡化方法4 隱藏內部協同事件兩個系統的fsm合成時，合成之前兩個系統的耦合點變成合成系統的內部事件點，合成之前分別出現在兩個系統中的協同事件變成合成系統的內部事件。內部協同事件根據需要可以隱藏，相關聯的狀態可以合并。隱藏內部協同事件的方法：41/893.2.4 fsm簡化方法4 隱藏內部協同事件隱藏內部協

18、同事件的方法：第一步：用i表示內部協同事件。如果 ， 并且e1和e2為協同事件，那么 ，i= 。第二步：合并關聯的兩個狀態。sisk合并成一個狀態，或重新定義成一個新狀態。sj是否消去，根據其它方法進行。tssjei1tsskej2tsskii42/893.2.4 fsm簡化方法5 通道fsm的簡化簡化原則原則1：如果n層協議實體采用同步通信方式(一問一答)，那么不管(n-1)層通道是否緩沖通道，都可以處理成非緩沖通道。原則2：如果報文傳送時間和延時時間對協議機制無影響，或者只影響協議變量的值，那么非緩沖通道可處理成空通道。43/893.2.4 fsm簡化44/893.2.5 fsm的合成全局

19、系統的fsm是由各個局部系統和通道系統的fsm合成的。合成過程1 簡化各個fsm2 兩個單工通道合成一個全雙工通道3 對任意兩個彼此耦合的系統合成中間合成系統，簡化中間合成系統，然后將中間合成系統再合成，直到獲得全局fsm為止。任意兩個耦合系統的fsm的合成步驟和規則：p4245/893.2.5 fsm的合成假定兩個fsm系統分別為f1=和f2=，合成后系統為f=。任意兩個耦合系統的fsm的合成步驟和規則：i=(i1,i2),其中，is，i1s1，i2s2。即，合成系統的初始狀態為兩個系統初始狀態的組合。s=s1*s2，如果ss1，rs2，那么(s,r)s，s的狀態數為s1和s2狀態數的乘積。

20、e=e1e2，如果e1e1，e2e2，那么e1e，e2e。e的事件數為e1和e2事件數之和。t=t1t2，如果 ，那么 ；如果 ，那么 ， t的轉換函數的數目為t1和t2數目之和。合成后，消去無用的狀態，必要時隱藏內部協同事件。11tssetrsrse), (),(122trretrsrse) ,(),(246/893.2.5 fsm的合成47/893.2.5 fsm的擴充純粹fsm只反映了協議事件和協議狀態之間的關系，不能表述最重要的協議元素：協議變量、協議行動、謂詞。擴充的fsm引入協議變量、謂詞和行動(對變量進行操作)使得fsm的轉換函數變得豐富而復雜。彌補了純粹fsm的不足。48/89

21、3.2.5 fsm的擴充擴充方法引入謂詞、行動用轉換函數 替代 ，t=e/p:a 。e表示輸入事件，ee；p表示謂詞；a表示行動(包括輸出事件，對變量進行的操作等)。如果系統從一個狀態到另一個狀態的轉換不包含輸入事件，t=p:a 。引入協議變量引入協議變量可以減少狀態數。協議行動對協議變量執行操作。如seq=(seq+1) mod 2。tssttsse49/893.2.5 fsm的擴充示例：引入協議變量seq，減少了狀態數。s狀態數53，r狀態數52。50/893.3 petri3.3 petri網網petripetri網概念網概念petripetri網特性網特性petripetri網擴充網擴

22、充協議實體協議實體petripetri網網通道通道petripetri網網petripetri網的替換與合成網的替換與合成協議并發性表示協議并發性表示51/893.3.1 petri網的概念petri網的提出1962年，波恩大學的c.a.petri提出一種可表示系統部件異步并發操作的網絡模型，后來取名為petri網。該模型已廣泛應用于計算機科學、電子學、機械學、化學、物理學等許多領域。也非常適合于協議模型技術。52/893.3.1 petri網的概念1 petri網定義petri網定義為一個五元系統，其中，p：位置(places)集，p=p1,p2,pi,t：轉換(transitions)集，

23、t=t1,t2,ti,i：輸入函數集，i=i(t1),i(t2), i(tj),，轉換tj的輸入函數i(tj)=pk,.,.plo：輸出函數集，o=o(t1),o(t2), o(tj),，轉換tj的輸出函數o(tj)=pm,.,.pnm：標記(marking)集，m=m1,m2,mk,，m0為初始標記，mk為第k次標記。標記mk為一個向量，mk=p1(n), p2(n), , pi(n), ，pi(n)為一個正整數，表示位置pi中的旗標數(tokens)。petri網的標記也叫petri網的狀態，m0為初始狀態，mk為狀態k，m為petri網的狀態集合。53/893.3.1 petri網的概念

24、1 petri網定義petri網的表示用圖形表示圓為位置，短線為轉換，連接圓和短線的有向弧為輸入函數或輸出函數，圓中的黑點為旗標。54/893.3.1 petri網的概念1 petri網定義petri網的示例55/893.3.1 petri網的概念1 petri網定義無界網及其狀態空間56/893.3.1 petri網的概念2 petri網的觸發規則petri網的特點之一是可運行性。petri網的運行由連續的觸發(firing)來進行。觸發規則當轉換tj的輸入函數i(tj)=pk, pl的所有位置都至少有一個旗標存在時，tj被觸發。tj觸發后，輸入函數的所有位置分別減少一個旗標，而輸出函數o(

25、tj)=pm,pn中的所有位置增加一個旗標。示例：3 petri網的狀態空間每觸發一次，狀態就變化一次，構成狀態序列，可用樹表示。57/893.3.2 petri網特性1 保守網2 有界網3 活動性4 并發與沖突58/893.3.2 petri網特性1 保守網如果一個petri網的每次觸發之后，輸出函數所增加的旗標數總是等于輸入函數所減少的旗標數，這種petri網叫保守網，反之叫非保守網。保守網的一個中重要含義是：如果旗標代表 一個系統的資源，那么該系統運行中不能自動生產這種資源，也不會丟失或消耗掉這種資源。2 有界網如果一個petri網運行中任何一個位置中的旗標數總是不超過k個，這種petr

26、i網就叫k階有界網，若某個位置的旗標數無限變大，就叫無界網。有界網的一個重要含義是：如果一個petri網的某個位置代表系統中的一個隊列，那么該隊列的最大允許長度為k。等等。59/893.3.2 petri網特性1階有界網k階有界網60/893.3.2 petri網特性3 活動性如果一個petri網在運行中，它的所有轉換都是潛在可觸發的，那么這個網有活動性。即，從初始標記m0開始，它的任何一個標記都有可能達到，或者從任何一個標記開始運行，它總能返回到初始標記。petri網的活動性的一個重要含義是：如果用它來表示一個協議，則它的活動性代表著協議活動性。61/893.3.2 petri網特性4 并發

27、與沖突多個轉換可并發(并行)觸發。協議并發所帶來的碰撞現象可通過petri網表達出來一個協議用petri網表示后，可通過研究petri網，設法提高協議功能的并發度，檢查并解決潛在的碰撞現象。62/893.3.3 petri網擴充前面所介紹的標準petri網難以表示協議性質、協議元素性質和通道性質。需要對其擴充，提高標準petri網的表達能力。擴充方面1 旗標和位置的擴充2 輸入函數和輸出函數的擴充3 轉換的擴充63/893.3.3 petri網擴充擴充方面1 旗標和位置的擴充標準petri網中，旗標沒有名字，沒有標識號。著色petri網(colored petrinet)允許一個位置中的多個旗

28、標有自己的名字或標識號，這樣可擴充旗標的表達能力。例如，當旗標表示系統資源時，著色旗標可表示不同的資源；當旗標表示報文時，著色旗標可代表內容不同的報文或順序號不同的報文。64/893.3.3 petri網擴充65/893.3.3 petri網擴充2 輸入函數和輸出函數的擴充打破標準petri網中輸入輸出函數在每個位置只減少或增加一個旗標的限制。在標準petri網中可引入邏輯“或”、“非”和“異或”關系，豐富轉換的觸發條件。著色petri網中，還可說明輸入函數中不同旗標之間的關系。如，圖(c)中轉換t的觸發條件66/893.3.3 petri網擴充3 轉換的擴充在轉換上標明謂詞和行動，這種pet

29、ri網叫謂詞行動petri網。67/893.3.4 協議實體petri網擴充的petri網有很強的靈活的表達能力，對于同一個協議實體，不同的人可以構造出不同的petri網。使petri網變得簡潔、形象直觀、含義準確的規則：用轉換表示協同事件，如a!m,a?m。外部輸入函數和輸出函數可用虛線表示。用轉換表示內部事件，如超時t和報文丟失drop等。轉換上擴充謂詞和協議行動用位置表示協議變量(窗口、序號、隊列等)和系統資源(緩沖區、連接數等)用位置中的旗標表示資源邊界(變量的取值范圍，緩沖區的緩沖器數等)盡量不用著色旗標表示資源的名字和標識號，因為著色旗標使petri網變得復雜。簡單的方法是采用謂詞

30、行動petri網。68/893.3.4 協議實體petri網對于ab協議，發端s只要設立一個send-buffer和ack-buffer，以及變量seq就可以運行。而收端r只要設立一個receive-buffer和變量seq就可以運行。下圖petri網分別表示s和r。位置和轉換的含義說明：s的位置：s1 send-buffer空 s2 send-buffer已接收一個報文 s3 send-buffer中報文已發送，等待認可 s4 ack-buffer中收到ack報文s的轉換：t1 a?m,seqm(m為數據報文) t2 a!m t3 a?ack t4 if ack=seq, seq=(seq+

31、1)(mod 2)s初始標記: s1中旗標表示：send-buffer空，s可以從a接收一個報文。69/893.3.4 協議實體petri網r的位置：r1 receive-buffer空 r2 receive-buffer中收到一個數據報文 r3 receive-buffer中組裝了一個ack報文r的轉換：t7 b?m (m為數據報文) t8 if m has error , drop m t9 b!ack t10 b!m, seq=(seq+1)(mod 2)r初始標記: r1中的旗標表示：receive-buffer空，r準備接收s發來的數據報文。70/893.3.4 協議實體petri網

32、71/893.3.5 通道petri網單工空通道等效于協同事件點，可表示為一個轉換。非緩沖通道單工非緩沖通道：全雙工非緩沖通道：用兩個單工petri網表示半雙工非緩沖通道：有發信權控制，比較復雜。緩沖通道：單工緩沖通道：全雙工緩沖通道：用兩個單工petri網表示72/893.3.5 通道petri網73/893.3.6 petri網的替換與合成用一個低層子系統的petri網替換高層系統petri網的一個位置或轉換的過程(或反過程)即petri網的替換。petri網的替換在協議模型技術中有兩種用法。一個協議實體的一個協議功能或模塊用一個位置或轉換表示，需要時用一個較細的petri網去替換它。通道只用一個位置或轉換表示，需要時再細化。將多個petri網合成一個大的petri網的過程即petri網的合成74/893.3.6 petri網的替換與合成petri網的替換75/893.3.6 petri網的替換與合成petri網的合成76/893.3.7 協議并發性表示實際的協議有強的并發性(并行性)。petri網很適合表示協議的并發性。iso t層協議(tp4)的數據發送過程為使t層數