基于SPIN內核的SDL模型檢驗工具設計

西昌 610005;3.中國電子系統設備工程公司研究所，北京 100141)

摘要:規格描述語言SDL目前廣泛應用于復雜通信協議和軟件系統的建模。使用模型檢驗技術對SDL進行分析和驗證可以檢測出模型中的邏輯錯誤，大大提高SDL建模結果的精確性。論文研究了SDL的形式化語義SDL/PR中常用部分與模型檢驗工具SPIN的輸入語言Promela之間的語義映射規則，并以此為基礎開發了一個基于SPIN內核的SDL模型檢驗器SSMC Tool。

關鍵詞:SDL; Model Checking;語義轉換;SPIN;模型驗證

中圖分類號:TP311文獻標識碼:A文章編號:1009-3044(2010)11-2624-03

Checking Tool Design of SDL Model Based on SPIN Kernel

HUANG Shan1，3， HUANG Zhong-jian2， HAN Ke3， WANG Jian-wei3

(1.Institute of Command and Control， PLA University of Science and Technology， Nanjing 210007， China; 2.The Mission Command and Control Center， Xichang Satellite Launch Center， Xichang 615000， China; 3.Institute of China Electronic Systems Equipment Company， Beijing 100141， China)

Abstract: SDL(Specification and Description Language)is widely applied in the modeling of complex communication protocol and software. Model checking can find out SDL's logic fault and greatly improve its accuracy. The paper has studied the mapping rule between SDL/PR and Promela，which is the input language of the model checker SPIN，and then programmed a SDL model checker SSMC Tool that is based on SPIN kernel.

Key words: SDL; Model Checking; semantic transition; SPIN; model verification

規格描述語言SDL(Specification and Description Language)[1]是ITU定義的一種數據類型支持能力極強的形式化描述語言，其核心基于擴展有限狀態機的通信進程模型。SDL目前大量應用于電信領域中的通信協議建模以及描述具備活性離散系統特征的軟件。模型檢驗(Model Checking)[2-3]是一種針對有限狀態系統的形式化自動驗證技術，自提出至今已被應用于計算機硬件、通信協議、安全認證協議等方面的分析與驗證中，取得了令人矚目的成績。使用模型檢驗技術對SDL模型進行分析與驗證，可以減少模型中的設計錯誤，提高建模的精確性[4]。對于SDL模型來說，如果對其直接模型檢驗，則需要重新構建專用的模型檢驗工具，這是一項十分煩瑣和困難的工作。將其轉換為某種模型檢驗工具的形式化輸入，則可以免去重新構建模型檢驗工具所需要的額外精力。出于以上因素考慮，本文研究了SDL模型的形式化文法SDL/PR[4]向模型檢驗工具SPIN的輸入語言Promela[2]的語義轉換規則，構造了文法翻譯器SDL2PromelaTranslator.exe，并設計實現了一個基于SPIN內核的SDL模型檢驗工具SSMC Tool。

1 文法翻譯器SDL2Promela的構造

1.1 SDL/PR到Promela的語義轉換規則

首先要實現系統結構的轉換。SDL的模型結構是形如System-Block-Process的層次性結構，而Promela中構建系統基本行為的單元是進程(proctype)，整個系統是一個由眾多進程構成的平面結構，但是二者的語義是一樣的，即以Process或進程為單位的有限狀態機之間的通信。因此我們將SDL/PR中的Process表示為Promela中的proctype。

其次要解決二種建模語言進程時間通信機制的轉換。在SDL中，Block和Block之間的消息通道是Channel，Process和Block以及Process之間通信的消息通道為 Signalroute。但是在SDL中，通信的實質是Process之間的通信，或者直接使用Signalroute作為通道，或者由幾個Channel和Signalroute組成一個組合通道傳遞消息。其目的是為了建模更具備層次性和易讀性，方便人們理解，因此在把SDL/PR文法映射為Promela語言的時候，需將層次性通信統一簡化為進程之間的直接通信。

最后需要實現SDL/PR中Process內部的FSM向Promela的proctype的轉換。Process內部的FSM分為四個部分:變量聲明、狀態變遷、收發消息、條件選擇。這四個部分在Promela的proctype中均可實現相應的等價映射。

根據上述轉換原則，得出具體的SDL/PR向Promela的轉換策略，如表1所示。

根據以上語義轉換規則，使用Lex和Yacc的集成工具Parser Generator2作為開發環境開發SDL/PR向Promela轉換的翻譯器。

Lex是一個詞法分析器，其作用是從頭到尾逐個字符地對輸入進行掃描，產生一個個的單詞符號，把字符串輸入變為單詞符號存入符號表，供語法分析器使用。

Yacc是一個語法分析器，功能是:在詞法分析器分析識別出單詞符號串的基礎上，分析并判定程序的語法結構是否符合語法規則，從而按照語法產生式，識別輸入符號串是否為一個句子，并在此基礎上對識別出的句子進行需要的操作，建立規定的翻譯。本文中要做的是在Yacc識別出SDL/PR的句子之后根據同Promela的轉換規則實施轉換。如圖1所示。

■

圖1 基于LexYacc的轉換過程圖

根據SDL/PR的語法編寫Lex文件，根據表1的語義編寫Yacc文件，之后在Parser Generator2工具下進行編譯，分別得到詞法分析器和語法分析器的C源代碼文件，再在VC++ 6.0環境下建立控制臺應用程序工程，加入C源代碼文件后進行編譯，得到翻譯器SDL2PromelaTranslator，可將SDL/PR轉換為相應的Promela模型。過程如圖2所示。

生成的翻譯程序為SDL2PromelaTranslator.exe文件，供SSMC Tool調用。

2 SDL模型檢驗工具SSMC Tool的設計與實現

2.1 系統設計思路與結構

SSMC Tool(Simple SDL Model Checking Tool)是一個自動將SDL/PR轉換為Promela，同時調用SPIN內核對模型進行分析和驗證的模型檢驗工具。其功能總的來說是讀取.sdl文件的內容，即系統SDL建模后得到的SDL/PR文法，將其轉換為SPIN的輸入語言Promela，之后調用模型檢驗工具SPIN的內核進行模型檢驗。可以說，這個原型工具是SDL/PRtoPromela翻譯器與SPIN內核整合的一個圖形化工具。工具具體的設計功能如圖3所示。

從圖中可知，系統設計了如下幾個重要功能塊:

圖形UI:為用戶提供便捷的圖形化操作方式，接收用戶的輸入信息，以及提供相關的錯誤信息提示。

參數設置模塊:以圖形界面形式，方便用戶對SPIN路徑、C編譯器路徑、SPIN運行命令等參數進行設置。

文件操作模塊:實現SDL/PR、Promela文件的打開、編輯及保存功能。

SDL/PR轉換模塊:將當前的SDL/PR模型自動轉換為Promela模型，SDL/PR模型和Promela模型分別保存在相對應的格式文件中。

SPIN調用模塊:調用模型檢驗工具SPIN完成語法檢查、LTL解析與轉換、模型的模擬運行、模型的性質檢驗等功能。

LTL模塊:接受輸入的LTL表達式，傳遞給SPIN。

C編譯器調用模塊:調用現存的C編譯器對模型檢驗器的C源代碼進行編譯，生成可執行的模型檢驗器。本工具使用gcc編譯器。

交互模擬控制模塊:對于交互模擬，以動態窗口的形式將可選項呈現給用戶，方便用戶的選擇和執行。

結果顯示模塊:獲取SPIN進行語法檢查、模擬和驗證的結果，并以適當的格式將結果顯示出來，還要調用顯示PS文件中的進程運行交互圖。

SPIN:模型檢驗工具SPIN的內核，包括LTL解析和轉換、核心算法等模塊。

2.2 系統關鍵技術

整個系統基于VC++6.0開發，在開發過程中涉及到的關鍵技術點如下:

SDL/PR到Promela的轉換。由于構建單獨面向SDL/PR的模型檢驗工具需要較大代價，本文根據SDL./PR同Promela語義之間的相似性，基于詞法和語法分析工具LexYacc構建了翻譯器SDL2PromelaTranslator.exe。這次轉換只涉及日常建模中常用的SDL元素，并沒有把ITU-T Z.100中對SDL的全部定義進行轉換。

進程調用的實現。在工具使用過程中，要調用SPIN進行語法檢查、模擬和驗證等操作，調用SDL2PromelaTranslator來進行SDL/PR到Promela的自動轉換。均采用進程調用的方法實現，具體使用WIN32API函數CreateProcess創建一個新的進程和它的主線程，這個新進程運行指定的SPIN可執行文件。如下:

CreateProcess(NULL，CommandLine.GetBuffer(1)，NULL，NULL，TRUE，NULL，NULL，NULL，sinfo，pinfo)

在具體的編程過程中，我們將調用SPIN的功能封裝為一個類模塊，提供調用SPIN的方法SPINRun(CString CommandLine，CString *ResultStr)，CommandLine即是存儲進程命令參數的輸入，*ResultStr則用來存儲返回的運行結果。

管道技術的應用。管道是進程通信中使用的共享內存的一部分。在調用SPIN過程中，要進行相關的命令參數輸入，也要收集其分析與驗證的運行結果，即要實現主進程與SPIN之間的數據交換。由于我們的主程序和SPIN之間存在親屬關系，因此使用匿名管道即可實現數據交換。需要創建兩個匿名管道，一個管道用于主程序向SPIN進行命令參數的輸入，另一個管道用于主程序從SPIN獲取運行結果。用CreatePipe函數創建一個匿名管道，返回兩個句柄:管道讀句柄和管道寫句柄。如下:

CreatePipe(hInReadPipe，hInWritePipe，sat，1024);

CreatePipe(hOutReadPipe，hOutWritePipe，sat，1024);

第一個管道是用于輸入的管道，hInReadPipe和hInWritePipe分別為管道讀句柄和管道寫句柄。第二個管道是用于接收輸出的管道，hOutReadPipe和hOutWritePipe分別是管道讀句柄和管道寫句柄。在進程調用的實現中提到，CreateProcess的參數sinfo是指向一個用于決定新進程的主窗體如何顯示的STARTUPINFO結構體，在這個結構體中，可以設定進程的讀寫句柄。如下:

sinfo.hStdInput=hInReadPipe;

sinfo.hStdOutput=hOutWritePipe;

通過上面的設定，當調用SPIN時，參數sinfo就指定SPIN從hInReadPipe讀數據，將運行結果輸出到hOutWritePipe。

交互模擬的實現。調用SPIN進行交互模擬是其重要的工作模式之一。在命令行下使用SPIN，其交互模擬的方式是呈現用戶一些選擇項，用戶輸入其中一個選項編號，SPIN則根據用戶選擇的路徑繼續執行，直至完成模擬工作。為了使用戶更加方便、高效地使用交互模擬進行模型的分析與驗證，我們采用動態窗口技術，將當前的可選項分別用一個按鈕表示，并全部顯示到一個動態窗口中，用戶可以通過點擊按鈕，方便地進行路徑的選擇和結束模擬，有效地控制了交互模擬運行。

PS文件的顯示。在SPIN的模擬運行過程中，可以通過參數“-M”來生成交互序列圖的PS格式文件，PS文件記錄了Promela中各進程的運行及與其它進程之間的交互情況。我們基于現有的gsdll32動態庫，通過調用其相關方法，可以實現模擬過程中的交互序列圖調用顯示。

2.3 系統設計與實現

系統的具體設計如圖4所示。

如圖所示，SSMC Tool主界面分為6個區域:

1)菜單區:包括包括“文件”、“編輯”、“轉換”、“設置”、“運行”和“幫助”六個菜單項。其中，“文件”項的功能是打開SDL/PR文件，并對轉換生成的Promela進行保存、另存為等操作;“編輯”提供常見的復制、剪切、粘貼等文本操作功能;“轉換”項功能調用SDL2PromelaTranslator.exe對SDL/PR進行轉換，轉換結果顯示在Promela源碼顯示區;“設置”、“運行”是調用模型檢驗器SPIN核心功能的圖形接口。

2)工具欄區:工具欄區的一系列圖標是菜單區每個下拉菜單中重要功能的快捷方式。

3)SDL/PR顯示區:這一區域用來顯示打開的SDL/PR文件，圖中顯示的是本文中游戲系統的SDL/PR部分源碼。

4)Promela源碼顯示區:這一區域負責顯示由SDL/PR自動轉換而得的Promela源碼，并可以對其進行二次編輯，圖中為生成的部分源碼。

5)LTL公式編輯區:用來輸入描述系統性質的線性時序邏輯公式，對于公式中符號的定義要在Promela模型中手工添加。

6)結果顯示區:這一區域負責顯示軟件的運行輸出，圖中顯示的是文獻[6]中猜謎游戲系統的分析驗證結果。

SMCC Tool具備生成的測試用例與原系統的交互模擬功能，便于測試人員在模擬過程中跟蹤測試用例的執行情況，如圖5所示。

3 結束語

SDL作為一種圖形化和形式化兼備的建模語言，正在得到愈加廣泛的應用。本文研究了其形式化語義同Promela的轉換關系，并據此設計和實現了一個基于SPIN內核的組件化SDL模型檢驗工具SMCC Tool。可實現SDL/PR模型到Promela模型的自動轉換;可方便調用SPIN對SDL模型進行分析與驗證。目前該工具盡支持部分常用SDL元素，增強對SDL負責模型的支持是下一步的研究重點，同時，將模型檢驗與軟件測試相結合[7]也是值得研究的方向。

參考文獻:

[1] ITU-T Z.100，Specification and Description Language(SDL)[S].

[2] Holzmann G J.The Model Checker SPIN[C].IEEE TRANSACTIONS ON SOFTWARE ENGINEERING，1997，23(5).

[3] 林惠民，張文輝.模型檢測:理論，方法與應用[J].電子學報，2002，30(12):1907-1912.

[4] 宋茂強.通信軟件設計基礎[M].2版.北京:北京郵電大學出版社，2008:166.

[5] Parser Generator Homepage[EB/OL].(2009-02-14).http://www.bumblebeesoftware.com/index.htm.

[6] Chang Chee-Kane.An Introduction to SDL[EB/OL].http://www.chu.edu.tw/~lhyen/files/cpe/IntroSDL.pdf.

[7] Gargantini A，Heitmeyer C.Using model checking to generate tests from requirements specifications[C].Proceedings of the 7th European Engineering Conference Held Jointly with the 7th ACM SIGSOFT International Symposium on Foundations of Software Engineering，Toulouse，FR，1999:146-162.