2.3MNMP的運行機製
為了保障MNMP運行時的安全性,在兩個MNMP管理實體要進行管理操作時,必須首先利用服務聯係原語在兩者之間建立應用聯係,聯係過程中完成狀態識別、身份認證、服務協商等操作。協議操作的具體運行步驟如下:
(1)請求方發聯係請求,提供必要的用戶信息和服務參數;
(2)服務方接收聯係請求,驗證用戶身份,驗證用戶身份和權限,進行服務參數的協商;
(3)服務方協商通過後,向請求方發聯係應答,返回延時修正值,並且提供全網唯一的聯係標誌,聯係建立;
(4)請求方在聯係已建立的基礎上進行管理操作,利用聯係標誌和延時修正參數構造操作PDU,發到服務方,如為有應答操作則等待服務方的應答;
(5)服務方解析接收到的操作PDU,根據請求方提供的參數提供服務操作,如為有應答操作則向請求方返回操作應答;
(6)請求方接收管理操作應答,決定是斷開服務聯係還是繼續進行下一次管理操作,雙方在規定的時間間隔進行聯係維護;
(7)管理操作結束後,雙方按照事先協商的方式斷開連接,並返回一些聯係統計信息。
3.MNMP的Petri網形式描述
MNMP的Petri網模型,網的初始標記Mo是TOKEN在P1(管理端等待發送聯係請求)和P6(代理端等待接收聯係請求)中。
4.1MNMP的Petri網可達樹分析
可達性分析是指生成Petri網的全部可達狀態,以檢查是否符合協議所要求出現的狀態以及期望的行為特征,通常包括死鎖、意外接收發送、變遷活性以及庫所標記數的有界性等。可達性分析從初始全局標識開始,根據每一個點活變遷或並發變遷集同時具備點火條件的變遷的集合生成分支結點,總體上形成可達樹。
通過可達樹的分析,我們可對協議的各種性質進行分析:
(1)有界性。可達樹中的每個節點中,每個位置中的標記數量都是有限的,所以此網是有界的;
(2)活性。從可達樹中可以看出,每個變遷至少被點火一次,不會出現死鎖;
(3)完整性。在描述中所說的狀態都能達到;
(4)前進性。可達樹中不存在無用的循環。
4.2MNMP的Petri網的不變量分析
不變量分析是要求網在特定執行模式下不變量的特性。Petri研究最廣泛且理論上最完備的兩種不變量是S—不變量和T—不變量。S—不變量對應於Petri網中標記總數保持不變的庫所子集,它反映協議的守衡性。T—不變量是指保持網標識不變的變遷序列,它反映協議運作的循環或重複特性。
4.2.1S—不變量分析
兩個庫所不變量表明,代理端、管理端,各自對應的所有庫所的token數等於常數1即各S不變量中的庫所對應的執行機構,在任何時候,隻有其中之一動作,信息在處理前,不會被再次傳送,從而保證了協議的可靠性。不依賴於初始標識,這代表代理端和管理端在協議運行過程中的庫所總量沒有發生變化,體現了協議的守恒性。
2.3MNMP的運行機製
為了保障MNMP運行時的安全性,在兩個MNMP管理實體要進行管理操作時,必須首先利用服務聯係原語在兩者之間建立應用聯係,聯係過程中完成狀態識別、身份認證、服務協商等操作。協議操作的具體運行步驟如下:
(1)請求方發聯係請求,提供必要的用戶信息和服務參數;
(2)服務方接收聯係請求,驗證用戶身份,驗證用戶身份和權限,進行服務參數的協商;
(3)服務方協商通過後,向請求方發聯係應答,返回延時修正值,並且提供全網唯一的聯係標誌,聯係建立;
(4)請求方在聯係已建立的基礎上進行管理操作,利用聯係標誌和延時修正參數構造操作PDU,發到服務方,如為有應答操作則等待服務方的應答;
(5)服務方解析接收到的操作PDU,根據請求方提供的參數提供服務操作,如為有應答操作則向請求方返回操作應答;
(6)請求方接收管理操作應答,決定是斷開服務聯係還是繼續進行下一次管理操作,雙方在規定的時間間隔進行聯係維護;
(7)管理操作結束後,雙方按照事先協商的方式斷開連接,並返回一些聯係統計信息。
3.MNMP的Petri網形式描述
MNMP的Petri網模型,網的初始標記Mo是TOKEN在P1(管理端等待發送聯係請求)和P6(代理端等待接收聯係請求)中。
4.1MNMP的Petri網可達樹分析
可達性分析是指生成Petri網的全部可達狀態,以檢查是否符合協議所要求出現的狀態以及期望的行為特征,通常包括死鎖、意外接收發送、變遷活性以及庫所標記數的有界性等。可達性分析從初始全局標識開始,根據每一個點活變遷或並發變遷集同時具備點火條件的變遷的集合生成分支結點,總體上形成可達樹。
通過可達樹的分析,我們可對協議的各種性質進行分析:
(1)有界性。可達樹中的每個節點中,每個位置中的標記數量都是有限的,所以此網是有界的;
(2)活性。從可達樹中可以看出,每個變遷至少被點火一次,不會出現死鎖;
(3)完整性。在描述中所說的狀態都能達到;
(4)前進性。可達樹中不存在無用的循環。
4.2MNMP的Petri網的不變量分析
不變量分析是要求網在特定執行模式下不變量的特性。Petri研究最廣泛且理論上最完備的兩種不變量是S—不變量和T—不變量。S—不變量對應於Petri網中標記總數保持不變的庫所子集,它反映協議的守衡性。T—不變量是指保持網標識不變的變遷序列,它反映協議運作的循環或重複特性。
4.2.1S—不變量分析