林廣榮,高時漢,褚慶昕(.廣州無線電集團廣州海格通信集團股份有限公司,廣州50663;.華南理工大學電子與信息學院,廣州 50640)
衛星移動通信協議層的實現和一致性測試方法
林廣榮1,2,高時漢1,褚慶昕2
(1.廣州無線電集團廣州海格通信集團股份有限公司,廣州510663;2.華南理工大學電子與信息學院,廣州510640)
自主衛星移動通信系統是基于GMR-1空口規范演進而來的同步軌道衛星移動通信系統,需要管理大量信道資源,支持無線資源分配、跨波束切換和業務連接管理等復雜流程,使得網絡協議層具有很高的復雜度。同時,該通信系統仍處于初期研發階段,尚無成熟的芯片/平臺可直接使用,需要自主進行終端和配套測試系統的開發。
1.1自主衛星移動通信系統的協議體系結構
自主衛星移動通信系統空中接口的協議體系可分為接入層和非接入層兩大部分,如圖1所示。其中,接入層由媒體接入控制層 (MAC)、無線鏈路控制層(RLC)、無線資源控制層(RRC)和分組數據匯聚協議層(PDCP)四個部分組成,非接入層則包括移動性管理層(MM/GMM)和連接/會話管理層(CM/SM)兩個部分。
在上述協議結構中,MAC和RLC層的用途是在移動地球站和信關站之間建立可靠的專用數據鏈路。RRC層則是用于管理無線接口的功能協議組,負責無線資源分配信息的交換以及越區切換信道的控制。
MM/GMM層是建立在RRC層之上,用于處理移動性和安全保密性的功能協議組,主要實現呼叫位置注冊、本地位置更新、入網鑒權、移動服務管理等功能。連接管理CM層,由呼叫控制(CC)、短消息業務(SMS)和補充業務3個部分組成。SM層則用于實現分組數據業務終端連接到外部數據網絡的處理過程。
1.2復雜協議的形式化描述
由于自主衛星移動通信系統的網絡協議層功能強大,復雜度高,需要研究有效的工程實現方法。用自然語言對協議進行描述具有不嚴格、不精確和有多義性的缺點。隨著網絡與分布式系統的迅速發展,通信協議的形式化(Formal Methods)技術獲得了長足的進步,其中,形式的描述與驗證是整個協議設計與實現的基礎,對協議實現的正確性、完全性和復雜度有至關重要的影響。目前主要的形式化模型包括有限狀態機FSM (Finite State Machine)模型和Petri網(Petri-Net)模型兩種。
有限狀態機是形式描述技術 (FDT,Formal Description Technique)的一種,也是多種形式化方法的基礎。FSM方法的直觀性強,可實現與其他形式化方法的組合和轉換,且易于自動實現,在FDT中占有重要地位。在協議一致性測試中,有限狀態機也是描述協議控制流最常用的形式化模型。
另一種重要的形式化模型是Petri網絡,這是德國學者C.A.Petri在其博士論文中首次提出的一種特殊的自動機模型,可用來描述通信系統中異步成分之間的關系,主要包括可達樹分析和矩陣方程分析兩種方法。借助Petri網的分析技術,能得到被模擬系統的有界性、安全性、守恒和可達性等方面的性能評價。但Petri網在刻畫復雜系統時異常繁瑣,也不利于描述協議的進展情況。因此,對自主衛星移動通信系統協議層的描述和實現采用基于有限狀態機的實現方法。
1.3基于FSM的協議層實現方法
本節以自主衛星移動通信協議層中移動性管理層的形式化描述、設計和實現過程為例,說明FSM方法的基本流程,其中包括:上下文定義、進程級分解、進程事件枚舉、進程事件響應和代碼級實現5個步驟。具體步驟如下:
(1)上下文定義:根據協議標準,MM層為上層(CM層)提供服務,以自身狀態和接收的消息為依據向對等實體發送消息實現狀態轉換,完成MM層實體的連接和釋放功能。如圖2所示。
(2)進程級分解:確定合適的進程模型。MM層的具體功能包括MM實體連接管理、位置更新管理和IMSI附著/去附著管理等,用單一狀態圖描述過于復雜,因此MM層的頂層狀態機模型采用父子復合型進程模型;而MM實體連接管理部分只涉及實體連接各狀態的轉換,可作為MM進程模型的子進程,其內部則采用單進程模型。

圖2 協議上下文
(3)進程事件枚舉:分析MM層實體連接相關的所有外部觸發和自觸發事件。MM層實體連接的觸發事件如圖3所示,包括:服務請求、服務終止、連接建立超時、低層錯誤、消息的發送和接收等。

圖3 協議觸發事件
根據協議觸發事件,列舉事件如表1所示:

表1 觸發事件列表
(4)進程事件響應:主要描述進程模型在不同狀態下對各種事件的響應行為,事件和行為由協議標準規定。設計中,首先從初始狀態出發,選擇一個所屬事件,根據事件選擇一個轉換條件并確定響應行為,以此確定目標狀態;然后根據協議標準,依次發掘遍歷所有狀態的所有事件和轉換條件。
表2是MM層實體連接進程模型在空閑狀態和等待MM連接狀態下的事件響應表。

表2 MM層實體連接進程事件響應表
(5)代碼級實現:根據協議標準,檢查事件響應表中的進程行為邏輯是否符合協議要求,確保功能完整無誤。然后畫出完整的狀態轉移圖,并按標準模板轉化為C++代碼。根據步驟(4)中的事件響應表描述,MM層連接實體管理狀態機如圖4所示。

圖4 MM層實體連接狀態轉移
2.1協議一致性測試介紹
協議一致性測試是一種黑盒功能測試。它根據協議的描述對協議的某個實現進行測試,判別協議的實現與所對應的協議標準是否一致。測試通過在特定PCO對被測實現的層間服務原語和協議數據單元進行控制和觀察來達到測試目的。PCO的全稱是控制觀察點,指測試系統和被測實現之間的通信點,測試系統通過PCO訪問被測實現并觀察通信結果。一致性測試包括本地測試、分布式測試、協調式測試和遠程式測試4種方法,如圖5所示。

圖5 四種協議一致性測試方法
圖5中,上/下測試器均為測試系統的一部分,其中上測試器在被測實現的上層控制PCO;下測試器則在低層控制PCO,同時給出測試判定;服務提供者是測試結構的一部分,為被測實現和下測試器提供通信環境,假設被測實現位于網絡體系結構的第N層,服務提供者為其提供N-1層的功能。
由于需要對研發的衛星通信終端整機進行協議一致性測試,所以不采用本地測試法。協調式測試法要求在上下測試器之間存在高度的測試協調,并對所收集和觀察到的信息進行報告,實現過于復雜,目前主要限于理論上的探討。分布式和遠程式測試方法的區別在于,前者要求被測實現必須暴露上邊界的服務訪問接口,而后者不要求能夠訪問被測實現的上邊界。因此,可根據被測實現上邊界PCO的可訪問情況,綜合使用這兩種測試方法。
2.2衛星終端協議一致性測試方法
根據協議一致性測試的要求,測試軟件的架構設計如圖6所示。軟件主要包括圖形化的測試管理界面、系統控制模塊和控制觀察點模塊3部分。其中,測試管理界面的主要功能包括測試結果顯示、測試例的選擇和參數配置;系統控制模塊則是測試軟件的核心模塊,用于調度整個測試過程的順利進行,包括根據用戶的選擇依次執行各測試例、封裝生成測試輸入數據單元、解析和判決測試輸出結果以及日志記錄等;PCO模塊用于實現測試系統與被測實現(被測終端)的通信。

圖6 協議測試軟件框圖
測試軟件劃分為兩個線程并發執行。其中,測試管理界面向測試人員提供圖形化用戶界面,并在測試開始后啟動測試調度線程執行測試,管理界面和調度線程之間通過網絡套接字進行同步。軟件采用模塊化設計,測試例集合、數據單元的封裝/解析和PCO模塊等與具體被測協議相關的部分,針對不同的被測協議有相應實現模塊。
一致性測試的流程如圖7所示。測試人員通過管理界面選擇測試例后,啟動調度線程,從測試例集合中根據選中的測試例、順序和執行次數進行執行。測試軟件通過控制觀察點向被測實現輸入測試序列,并比較輸出響應與預期是否一致,最后在管理界面上顯示判決結果。

圖7 測試執行流程
2.3協議一致性測試結果
自主衛星移動通信空口規范對移動性管理層給出了43項測試例,根據上述測試方法選中全部測試例對1.3節中MM子層協議實現的測試結果如表3所示。

表3 移動性管理層協議一致性測試結果
本文介紹了目前主要的協議形式化技術和一致性測試方法,針對自主衛星移動通信系統中協議層的工程化實現問題,提出了一種基于有限狀態機的協議實現方法,并對系統空口規范中的移動性管理子層進行了實現和一致性測試。測試結果表明,代碼實現符合所有協議一致性測試項,從而驗證了上述方法的正確性和完備性。
[1]鄭林華,韓方景,聶皞.衛星移動通信原理與應用[M].北京:國防工業出版社,2000:4-7.
[2]GMR-1 01.202(ETSI TS 101 376-1-3)-2001:"GEO-Mobile Radio Interface Specifications;Part 1:General Specifications;Sub-part 3: General System Description"[S].France:ETSI,2001.
[3]肖德琴,沈勇,張建偉.網絡通信協議形式化描述與驗證技術的研究[J].重慶師范學院學報(自然科學報),1997,14(2):69-75.
[4]馮玉龍,張偉.基于衛星移動通信的網絡移動建模[J].計算機工程,2008,34(12):246-249.
[5]黎文導,盧瑜.有限狀態機(FSM)的實現[J].青海師范大學學報,2001(4):18-21.
[6]李臘元.基于FSM的通信協議形式描述與驗證技術[J].系統工程與電子技術,1990(9):40-47.
褚慶昕(1958-10),男,山東人,博士,教授,研究方向是射頻電路與天線研究
Satellite Communication;Network Protocol;FSM;Conformance Test
Implementation and Conformance Test of Satellite Mobile Communication Protocol Layer
LIN Guang-rong1,2,GAO Shi-han1,CHU Qing-xin2
(1.Guangzhou Haige Communications Group Incorporated Company,Guangzhou 510663;2.School of Electronic and Information Engineering,South China University of Technology,Guangzhou 510640)
1007-1423(2016)18-0050-05
10.3969/j.issn.1007-1423.2016.18.012
林廣榮(1980-),男,廣東饒平人,博士,工程師,研究方向為衛星與無線通信
高時漢(1966-),男,安徽人,碩士,高級工程師,研究方向是衛星通信系統架構
2016-04-14
2016-06-15
自主衛星移動通信系統需要管理大量的信道資源和業務流程,其網絡協議層具有很高的復雜度。為了對其進行工程實現,對協議的形式化技術進行研究,給出一種基于有限狀態機的網絡協議實現和一致性測試方法,并通過自主衛星移動通信網絡協議中移動性管理子層的開發和測試進行驗證。一致性測試的結果表明,上述方法能夠有效保證協議層實現的正確性和完備性。
衛星通信;網絡協議;有限狀態機;一致性測試
Satellite mobile communication system administrates substantial channel resources and traffic procedures,which leads to the high complexity of system network protocol.By studying the protocol's formal methods,presents engineering schemes of network protocols’development and the conformance test based on FSM.Furthermore,puts the schemes into practice by realizing the mobility-management layer in satellite mobile communication protocol stack.Results of conformance test indicate that the above solution can guarantee the validity and completeness of protocol realization.