基于SPIN的HMSC模型自動檢驗方法

李立亞，孫雨荷，馬漢杰+，丁佐華，黃鴻云

(1.無錫科技職業(yè)學院 人工智能學院，江蘇 無錫 214000；2.浙江理工大學 計算機科學與技術學院，浙江 杭州 310018；3.浙江理工大學 圖書館多媒體大數(shù)據(jù)中心，浙江 杭州 310018)

0 引 言

需求分析是軟件開發(fā)過程中的重要一環(huán)，需求通常以自然語言進行描述，但是由于缺乏形式化的定義，其正確性很難驗證?；谖谋拘枨髐se case建立HMSC(high-level message sequence chart)模型，能夠幫助用戶跟蹤應用程序的控制流，將軟件系統(tǒng)的通信行為以非常直觀方式進行展示。而對建立的HMSC模型進行正確性檢測與驗證是保證文本需求被正確建模必不可少的工作。在現(xiàn)有的研究中，有許多模型檢驗的方法，然而它們主要存在的問題是在分析中需要過多人為參與，不能實現(xiàn)自動化。在本文中，我們提出了一種自動檢測HMSC模型的方法。首先建立了HMSC模型到Promela檢測語言的轉換規(guī)則，并提出了自動轉換算法，從而實現(xiàn)了為HMSC模型生成Promela代碼。然后，利用模型檢測工具SPIN對Promela描述的模型進行正確性驗證，同時能夠檢驗HMSC模型是否滿足文本需求設計。此外，本文實現(xiàn)了一個對文本需求進行自動建模以及驗證分析的工具，并通過一個實例(EIRENE)展示了該工具在自動建模及檢測方面的效果。總的來說，我們的方法具有以下3點優(yōu)勢：①SPIN工具結合Promela模型語言能夠完成模型檢驗，并通過對系統(tǒng)行為的動態(tài)模擬可以實現(xiàn)需求的合理性分析；②整個模型驗證過程實現(xiàn)了自動化；③我們的建模及檢測分析工具整合了SPIN的功能，可以驗證任意LTL公式。

1 相關工作

1.1 HMSC模型

從需求文本中提取信息并轉化為形式化的模型，有利于對需求的驗證與管理[1]。針對需求文本use case建模的方法和工具有很多。例如，將文本use case轉換成UML中的模型[2]。除了UML外，MSC(message sequence chart)也可為需求use case建立行為模型[3]。

MSC是一種受歡迎的軟件系統(tǒng)行為圖形描述語言[4，5]。單個MSC用于描述系統(tǒng)的局部行為，其中，實例(Instance)表示軟件系統(tǒng)的各組件、用戶或外部環(huán)境，以垂直箭頭表示。實例間的交互稱為消息，用水平箭頭從消息的發(fā)送者指向接收者。事件(Event)是指消息箭頭開始的點(發(fā)送事件)或結束的點(接收事件)。

HMSC將多個簡單的MSC進行組合關聯(lián)，以描述系統(tǒng)的整體行為[5，6]。HMSC利用choice、sequential和loop操作將多個MSC關聯(lián)到一起，choice代表選擇操作，sequential表示順序操作，loop表示循環(huán)操作。在圖1中，我們給出了一個HMSC示例，其中單個MSC用長方形方框表示，而HMSC通過控制流操作將它們組合在一起。

圖1 HMSC中的sequential、choice以及l(fā)oop操作符

1.2 模型正確性檢測

模型檢測是軟件質量保障的一重要環(huán)節(jié)，從20世紀80年代開始了模型檢測的相關研究[7]。Clarke等[8]最早提出用CTL邏輯來描述并發(fā)系統(tǒng)性質。基本思想是將軟件系統(tǒng)的某些性質用時序邏輯來描述，并在描述系統(tǒng)的有限狀態(tài)集合中檢查這些性質是否被滿足。其中，計算樹邏輯(CTL)、有線性時序邏輯(LTL)以及命題μ-演算等都可以作為模型檢測時使用的時序邏輯。同時，也誕生了SMV[9]、SPIN[10]、CWB[11]和UPPAAL[12]等眾多模型檢測工具。

在這些工具中，基于SPIN的驗證在學術界和工業(yè)界被廣泛使用[13]。由于SPIN良好的算法設計和較強的檢測能力，本文也使用其作為檢測工具?；赟PIN進行的模型檢測研究也非常多，Ji等[14]將UML類圖、狀態(tài)圖和協(xié)作圖轉換成verification model，并為其生成Promela代碼，進而通過SPIN完成模型檢測；Krook等[15]通過SPIN對汽車自動駕駛系統(tǒng)的控制算法進行驗證；Bai等[16]將SPIN 用于驗證智能合約模板的正確性和必要屬性。

2 基于SPIN的HMSC模型檢測方法

2.1 SPIN檢測過程

SPIN工具通過never claims、斷言(assertion)以及特殊的標記3種方式來實現(xiàn)對軟件系統(tǒng)的正確性檢測，其中正確性包括了不發(fā)生死鎖情況和不存在活性問題，斷言永遠為真以及滿足自定義的LTL公式。

Promela是一種用來驗證并行系統(tǒng)邏輯正確性的進程模型語言[17]。一個用Promela描述的軟件行為模型，SPIN可以通過對其進行隨機或者迭代模擬執(zhí)行來驗證模型的正確性，或生成C程序對系統(tǒng)的狀態(tài)空間進行窮舉檢查。Promela程序由processes、message channels和variables組成[18]。其中，processes定義了系統(tǒng)的行為，而channels和variables制定了processes運行的環(huán)境。

本文按照典型的SPIN工作模式來完成檢測過程。首先，使用Promela語言為并發(fā)系統(tǒng)構建高層次的行為模型，在確認沒有語法錯誤之后通過SPIN的交互模擬功能驗證系統(tǒng)的設計行為是否符合預期。然后，SPIN為其生成一個自定義的on-the-fly驗證程序并進行編譯，進而驗證模型中各種正確性斷言是否成立(例如LTL公式)并給予用戶反饋。

2.2 HMSC模型的Promela實現(xiàn)

由于HMSC是由多個簡單MSC組合關聯(lián)而成的，因此需要為基本MSC以及HMSC間的選擇和循環(huán)結構實現(xiàn)Promela表示。也就是說，在HMSC的Promela代碼實現(xiàn)過程中，需要解決兩個問題：一是對于基本MSC(不包含HMSC中操作符的MSC，也稱Basic MSC)中描述的有限執(zhí)行序列如何用Promela表示；二是對于HMSC中的選擇和循環(huán)結構如何用Promela表示。此外，還需要為MSC中的Instance選擇通信通道以及設定容量。

2.2.1 Basic MSC的Promela實現(xiàn)

為了完成MSC的Promela代碼實現(xiàn)，首先在系統(tǒng)的啟動階段，為每一個MSC中的instance建立一個process，并且在init代碼塊中啟動所有的processes。對于不止一個process的情況，需要使用atomic代碼塊以保證所有processes啟動的原子性，例如，設某MSC有兩個instances P1 和P2，在init代碼塊中，需要這樣寫：atomic{run P1()；run P2()；}； 在MSC和Promela中，消息是有類型的，使用mtype表示消息的類型。 mtype={a，b} 表示兩個一字節(jié)整數(shù)常量a和b，且a=1，b=2，即創(chuàng)建了兩種消息類型a和b。

在為MSC建立基于Promela的行為模型時，選擇容量為1的channel作為processes中間通信的通道，并且對于MSC中的每一個消息箭頭，都有一個通信通道與之對應。channel中的消息類型必須與MSC中event處理的消息類型相同，在Promela中，使用 “chan ch=[1]of {byte}” 定義一個名稱為ch容量為1接收消息類型為byte的消息通道，對應于MSC中的消息通道，byte需要根據(jù)實際情況替換成對應通道的消息類型?？偨Y來說，將basic MSC轉化為Promela步驟如下：

步驟1 必要的數(shù)據(jù)定義，包括全局channel定義等；

步驟2 通過proctype關鍵字為每一個instance獨立定義process，在本文介紹的模型中所有process沒有需要接受的參數(shù)。

步驟3 在init代碼塊中啟動每一個process。

2.2.2 選擇和循環(huán)結構的Promela實現(xiàn)

Basic MSC的Promela實現(xiàn)后，需要將HMSC中的選擇或者循環(huán)結構用Promela代碼描述。圖2是一個包含選擇結構的HMSC。通過前面的方法，我們將MSC中的每一個instance都轉換為了process。在圖2中，當P1發(fā)送完消息req之后，P2可能回復success消息也可能回復failure消息。

圖2 包含選擇結構的HMSC

這里有4個基本的執(zhí)行指令，分別是：P2發(fā)送success、P2發(fā)送failure、P1接收success和P1接收fai-lure。要確保P2發(fā)送success之后，P1必須要接收該success消息。同樣，P2發(fā)送failure之后，P1必須要接收該failure消息，這里的一個操作涉及到了兩個進程。也就是說，用Promela實現(xiàn)HMSC中的選擇或者循環(huán)結構時，P1和P2之間需要進行同步。但是Promela語言中并沒有直接提供同步組件，我們需要自己獨立實現(xiàn)。

圖3 選擇結構的HMSC的Promela實現(xiàn)

2.2.3 HMSC模型到Promela代碼的自動轉換

HMSC模型到Promela代碼的轉換方法的UML類圖如圖4所示。其中，有兩個非常重要的類，一是Promela-Generator，該類主要提供了對外的使用接口，通過構造函數(shù)傳入HMSC模型，通過generate()方法生產Promela代碼；另一個是PromelaModel類，相當于Promela語言的模型類，它以組合的方式包含了Promela中的大部分特性。例如，Promela中的變量定義被抽象成了Variable類，消息通道的定義被抽象成了Channel類等。這些代表語言語法的類通過組合關系被添加進了PromelaModel中，我們只需要對PromelModel進行操作，就可以自動獲得映射好的Promela代碼。以下是這些實現(xiàn)類中的重點方法。

(1)Process類

Prcocess類有3個屬性，分別是表示該Process名稱的name，所有選擇或者循環(huán)操作符跳轉點的集合gotoPositions以及該Process所對應的Promela代碼緩存區(qū)sb。

另外，該類有兩個關聯(lián)的類IfWait和IfSignal，這兩個類是上文中介紹的在Promela中自己實現(xiàn)的同步組件，用以實現(xiàn)選擇和循環(huán)結構。IfWait類用于生成wait代碼段，而IfSignal用于生成signal代碼段。

在Process類中還提供了一系列公有方法，如addSendMessage()用于向當前的process中添加消息發(fā)送語句，而消息通道和消息的類型則通過方法參數(shù)傳遞進來；addGotoPoint()用于添加跳轉點；addIfSignal和addIfWait分別用于添加signal代碼段和wait代碼段。

(2)Init、Define、Channel、Variable、LTL和MType類

Init類表示Promela中的init代碼段，用于啟動創(chuàng)建的process，其中方法addProcess()可以將一個Process添加待啟動的列表中；Define表示Promela中的define語句；Channel表示Promela中的消息通道定義語句；Variable表示Promela中的變量定義語句；LTL表示Promela中的LTL公式，addLTL()將一個LTL公式添加到代碼中；MType類表示Promela中的mtype語句。

(3)PromelaModel類

Promela類組合了Init、Define、Channel、Variable、LTL、MType和Process類，通過組合它們的功能而構成了整個Promela模型。getPromela()方法可以得到對應的Promela代碼。

(4)HMSCWrapper類

HMSCWrapper是一個HMSC的包裝類，它主要是為HMSC提供一些便捷的操作接口。例如isJump()方法判斷當前節(jié)點是否是一個跳轉節(jié)點；isLoop()方法判斷當前節(jié)點是否是循環(huán)結構的起始節(jié)點；getNextNode()方法返回當前節(jié)點的下一個節(jié)點(順序操作符的next屬性指向的節(jié)點)；getBranchNode()方法返回當前節(jié)點的分支節(jié)點(如選擇操作符或循環(huán)操作符的child02屬性)。

(5)HMSCNode類

HMSCNode是HMSC模型中Node類的輔助類，主要用于Node的一些判斷操作。例如isHMSC()方法判斷該Node是否是HMSC；getHMSC()方法返回該Node對應的HMSC。

(6)PromelaGenerator類

該類主要對外提供操作接口，通過generate()方法可以獲得生成的HMSC的Promela實現(xiàn)。

3 工具實現(xiàn)

本節(jié)將介紹根據(jù)前文介紹的方法，實現(xiàn)的一個文本需求use case自動建模及檢測分析工具。

3.1 框架介紹

該工具的主界面如圖5所示，整個界面分為3個部分，左上為HMSC可視化圖形接口，右側欄為LTL公式輸入以及SPIN分析結果輸出接口，而下方為各種操作的接口。

圖5 工具主界面

在下方的操作接口中，一共有4組，每一組都有一個標簽，它們分別是NLP、Usecase、HMSC和ModelChec-king，下面分別簡要介紹其功能。NLP標簽中的功能實現(xiàn)了自然語句句法解析樹的管理，其中預置了支持的語法，也可以自定義進行添加。Usecase標簽中的功能主要實現(xiàn)了文本需求use case的自動建模，它以文本需求use case為輸入，借助自然語言處理工具和預先存入的語法解析樹，自動生成use case靜態(tài)模型。HMSC標簽中的功能實現(xiàn)了從use case靜態(tài)模型到HMSC動態(tài)模型的自動轉換，HMSC除了圖形化顯示還可以預覽其XMI文本。Model Checking標簽的功能實現(xiàn)了HMSC模型的自動驗證，它可以為HMSC模型自動生成Promela代碼，同時整合了SPIN，完成模型檢測功能，在右上的文本框里，還可以輸入LTL公式進行驗證。下面重點介紹Model Checking部分的功能。

3.2 模型檢測

在ModelChecking標簽中，有兩個功能按鈕，分別是Promela和Spin。Promela用于自動將HMSC模型轉換為Promela模型，Spin按鈕集成了模型檢測工具SPIN用于模擬執(zhí)行Promela，并輸出結果，如圖6所示。而位于主界面右上的LTL窗口中，LTL Formula用于輸入合法的LTL公式，Check用于檢測該Promela模型是否滿足該公式，其驗證結果將在Output文本顯示框中顯示，如圖7所示。

圖6 Promela自動生成窗口

3.3 應用場景

利用這個工具可以對多線程軟件進行有效的檢測。比如檢測一個網(wǎng)上購物商城系統(tǒng)，該系統(tǒng)由許多業(yè)務子系統(tǒng)組合而成，各業(yè)務子系統(tǒng)之間通過通用接口進行交互，完成一次特定的功能。此時，對于用戶的一次購物操作，其涉及的子系統(tǒng)包括商品主數(shù)據(jù)系統(tǒng)、商品分類系統(tǒng)、購物車系統(tǒng)、用戶登錄系統(tǒng)、訂單中間件和支付系統(tǒng)。我們可以將以上過程涉及到的任意use case輸入到工具中，為其自動建立HMSC模型，并進行驗證。如果模型檢測結果輸出窗口中出現(xiàn)錯誤信息提示，則根據(jù)具體信息進行判斷，從而對文本需求use case進行修改，以在軟件開發(fā)的需求工程階段找到并解決錯誤。此外，該工具也可以檢測協(xié)議、驗證算法的正確性和線性時態(tài)邏輯的正確性，因此，具有較為廣泛的使用場景。

4 實例分析

我們借助一個實例驗證本文提出的方法。該實例來自EIRENE(european integrated railway radio enhanced network)的功能需求規(guī)范。EIRENE是一種鐵路通信網(wǎng)絡，其功能需求規(guī)范則定義了一個滿足歐洲鐵路無線通信需求的無線電系統(tǒng)，它包括地面列車的語音和數(shù)據(jù)通信，以及地面軌道工人、車站、倉庫工作人員和鐵路管理人員之間的移動通信。

Cab Radio是這個功能需求規(guī)范中描述的一部分，包括driver call功能、與driver相關的其它功能、與cab radio相關的其它功能、環(huán)境需求和物理需求、driver的人機接口、driver的安全設備接口、列車車載記錄器、控制/命令接口以及其它相關接口。我們以driver call功能相關的Send Railway Emergency Call(發(fā)送鐵路緊急呼叫)為例，這一功能涉及3個子系統(tǒng)：cab radio，MMI(man-machine inteface)和driver，圖8給出了它們之間的關系。該用例的場景如下：為了進行鐵路緊急呼叫，driver需要通過MMI設備發(fā)送(接收)信息，首先driver通過MMI初始化一個呼叫，呼叫信息會傳遞給cab radio，同時該信息也會發(fā)送到與cab radio連接的列車車載記錄器，cab radio在接收到呼叫請求后將會開始進行連接，當driver接收到連接信息后將會向MMI發(fā)送一個消息，并且當driver拿起話筒時，呼叫連接將會接通到LoudSpeaker。最后，當呼叫結束時，driver將會終止至此呼叫，當cab radio接收到終止信號時，將會發(fā)送一條指示消息，這條消息將會通過MMI發(fā)送給driver。

圖8 Send Railway Emergency Call關系

我們使用3個use case描述這個場景，如圖9所示。接下來，利用上文介紹的工具，并按要求以這些用例作為輸入，讓工具自動生成HMSC模型，并進行檢測。其結果如圖10所示。

圖10 實例生成的HMSC

在以上實例中，HMSC圖形中的每一個節(jié)點都是一個MSC，我們可以通過點擊每個節(jié)點以查看其具體內容。而在右側的輸出窗口中，可以發(fā)現(xiàn)SPIN的模型驗證輸出結果。根據(jù)SPIN輸出結果分析，可知該模型不存在invalid end states，即沒有死鎖等非法狀態(tài)。同時，也可以驗證LTL公式是否滿足需求，例如對于公式 “[]<>mmi_10==0” 表示，mmi沒有收到checks connection請求(Use case 2中的“6 System checks connection”)。將該LTL輸入后對其進行驗證，其輸出結果如圖11所示。根據(jù)LTL輸出結果含義，可知該次模型驗證過程啟用了never claim，即輸入的LTL公式。同時該次執(zhí)行檢測到了一個錯誤，該錯誤表示該LTL公式不能得到滿足，即該模型不滿足此LTL公式表達的性質。

圖11 LTL輸出結果

同時，該工具可以得到自動生成的HMSC的Promela代碼實現(xiàn)。首先點擊 “Promela”按鈕然后點擊“Generate”按鈕，其自動生成的部分Promela代碼如圖12所示，其中所生成的Promela代碼一共有824行之多。借助SPIN的可視化工具ispin還可以對該Promela代碼進行執(zhí)行模擬，觀測其行為軌跡。圖13顯示了該Promela代碼某次執(zhí)行的軌跡圖。

圖13 實例的Promela代碼某次執(zhí)行軌跡

5 結束語

本文針對由文本需求use case建立的HMSC模型的正確性檢測與驗證提出了一種方法。提出從HMSC模型到Promela模型檢測語言的轉換規(guī)則，以及其實現(xiàn)算法，進而將HMSC模型轉換為Promela代碼并進行模型檢查，并借助SPIN完成需求的正確性驗證。同時基于以上方法實現(xiàn)了一個文本需求use case自動建模及檢測分析工具。我們的工作為HMSC模型的驗證提供了完整可行的方法和工具。整個過程都是自動的，不需要過多的人為參與，縮短了建模和分析的時間，大大提升了軟件開發(fā)效率。

本文提出的這些方法以及其工具實現(xiàn)能很好完成HMSC模型的檢測。但仍然還有一部分工作，需要更進一步的研究與完善。其中模型檢測的結果不能自動反饋至文本需求use case中，而需要人參與分析。后續(xù)我們還會圍繞這些方面開展進一步的研究工作。