張濤，黃少濱，黃宏濤，呂天陽，劉剛

(哈爾濱工程大學(xué)計算機科學(xué)與技術(shù)學(xué)院，黑龍江哈爾濱150001)

需求設(shè)計中的各種錯誤與不一致會為系統(tǒng)開發(fā)帶來巨大的成本開銷［1］，因此需求有效性驗證已成為軟件工程的一個重要研究領(lǐng)域.對于并發(fā)系統(tǒng)，由于其內(nèi)部通信活動的復(fù)雜性［2］，極大地增加了需求設(shè)計的驗證難度.目前還沒有通用的需求驗證模式，驗證工作大致可以分為兩大類［3］:需求不一致性管理框架和需求的驗證分析及處理策略［4-5］.模型檢測［6］是一種形式化驗證過程中面向有窮狀態(tài)并發(fā)系統(tǒng)的自動分析和驗證技術(shù)，其使用遷移系統(tǒng)建模并發(fā)系統(tǒng)，模態(tài)/時序邏輯建模系統(tǒng)規(guī)范，當(dāng)系統(tǒng)模型違反規(guī)范時，模型檢測工具將導(dǎo)致錯誤結(jié)果的事件序列作為反例返回給用戶，為系統(tǒng)漏洞定位和改進提供幫助，目前最為常見的模型檢測工具是SMV［7］和 SPIN［8］.目前，一些研究使用模型檢測器SMV自動驗證系統(tǒng)需求設(shè)計的一致性［9-11］，但是SMV對于驗證軟件系統(tǒng)的異步通信行為的效果不如SPIN，其反饋給用戶的錯誤跡是一系列執(zhí)行路徑上狀態(tài)變量的值，這種類似于文本行輸出的錯誤路徑只能跟蹤系統(tǒng)狀態(tài)的變遷，無法像SPIN一樣顯示并發(fā)對象間的通信行為.為此，一些研究使用模型檢測器SPIN驗證系統(tǒng)需求設(shè)計的正確性［12-14］，通過自定義轉(zhuǎn)換規(guī)則將需求模型轉(zhuǎn)換為PROMELA程序，并將系統(tǒng)需要滿足的各種性質(zhì)規(guī)約抽象為線性時序邏輯公式，最后使用SPIN自動驗證PROMELA模型是否滿足線性時序邏輯公式.此類研究方法中存在的問題是:需求模型到PROMELA程序的轉(zhuǎn)換過程或是非全自動的，或是不完全的，且在轉(zhuǎn)換后的狀態(tài)空間中引入了冗余.針對上述各問題，本文提出一種基于場景［15］的并發(fā)系統(tǒng)需求驗證方法，用UML順序圖建模并發(fā)系統(tǒng)需求場景，通過定義順序圖的形式化操作語義及轉(zhuǎn)換規(guī)則，將順序圖的XML文件自動的轉(zhuǎn)換為對應(yīng)的Promela程序，將系統(tǒng)需要滿足的性質(zhì)規(guī)約抽象為線性時序邏輯公式，用模型檢測器SPIN自動驗證并發(fā)系統(tǒng)需求設(shè)計的一致性和完備性.

1 UML順序圖的形式化定義

UML 順序圖(UML sequence diagrams，SD)［16］用于描述軟件系統(tǒng)的需求設(shè)計，提供系統(tǒng)的期望場景和異常場景，展現(xiàn)并發(fā)對象動態(tài)行為交互［17］.順序圖的基本元素是對象與消息流，帶有矩形的垂直虛線表示圖中對象，矩形內(nèi)標(biāo)有對象名稱，垂直虛線稱為對象的生命線，表示特定時間段內(nèi)對象的存在.生命線上自上而下依次排列一系列事件，主要包括消息發(fā)送事件、消息接收事件等.從消息發(fā)送事件指向消息接收事件的帶箭頭水平直線或斜線表示消息，根據(jù)事件間的序關(guān)系可以從順序圖中得到一組消息序列.下面給出UML順序圖的形式化定義:

定義1(UML 順序圖，SD).SD=(O，C，E，M，F(xiàn)，D)是一個六元組，其中:O為對象的有窮集合.V={v|?o∈O，v∈Var(o)}為 SD 的變量集合，Var(o)表示對象o∈O的變量，Eval(v)為變量v的求值函數(shù)，Cond(V)為變量集V上的布爾條件集合.C是信道的有窮集合，對于信道?c∈C，cap(c)表示信道的容量，cap(c)=0表示順序圖中并發(fā)對象在信道c上執(zhí)行同步通信，cap(c)表示并發(fā)對象在信道c上執(zhí)行異步通信，Eval(c)為信道c的求值函數(shù).E為事件有窮集合，每個事件對應(yīng)消息在信道上的發(fā)送或接收.M為消息有窮集合，對于信道c∈C，對任意的消息m∈M，分別用c!m和c?m表示向信道發(fā)送消息和從信道接收消息.任意事件e∈E，其或是某一消息m的發(fā)送事件或是接收事件，分別表示為λ(e)=m!m或λ(e)=c?m.F∶E→O是一個映射函數(shù)，將每一個事件e∈E映射到唯一的一個構(gòu)件上F(e)∈O.D?E×E是事件集合上的偏序關(guān)系，每個(e，e')均滿足 e≠e'，(e，e')描述 SD 中事件e和e'間的先后順序.

2 UML順序圖的操作語義

在模型檢測中使用遷移系統(tǒng)和程序圖建模系統(tǒng)行為，定義如下:

定義2 遷移系統(tǒng)(transition system，TS)［18］.遷移系統(tǒng)是一個六元組:TS=(S，Act→，I，AP，L)，其中:

S是系統(tǒng)狀態(tài)的有窮集合.Act是動作的有窮集合.→?S×Act×S表示遷移關(guān)系.I?S是系統(tǒng)初始狀態(tài)的有窮集合.AP是原子命題的有窮集合.L∶S→2AP是一個標(biāo)簽函數(shù).

定義 3 程序圖(program graph，PG)［18］.在變量集合Var上定義的程序圖是一個六元組，PG=(loc，Act，Effect，→，loc0，g0)，其中:

loc是圖中所有位置的集合.Act是所有動作的集合.Effect∶Act×Eval(Var)→Eval(Var)是一個函數(shù)，表示動作對變量值的影響.→∶Loc×Cond(Var)×Act×Loc表示條件遷移關(guān)系，即一個位置滿足一定條件執(zhí)行動作后可達另一位置.loc0?Loc是初始狀態(tài)集合.g0∈Cond(Var)是初始條件.

程序圖主要用來刻畫系統(tǒng)對象行為的動態(tài)變遷，本文為順序圖SD中的每一個對象定義一個相應(yīng)的程序圖元組，即對于?oi∈O，i?0，在變量集合Var(Oi)上有 PGi=(Loci，Acti，Effecti，→i，loc0i，g0i)，其中:

Loci是對象oi所有位置的集合，除初始位置外，對象每接收或發(fā)送消息時產(chǎn)生一個位置.Acti={c?m，c!m，τ}是對象 oi的動作結(jié)合，其中 τ表示內(nèi)部動作，一個位置在執(zhí)行內(nèi)部動作后停留在原位置.Effect∶Acti× Eval(Var(oi))→Eval(Var(oi))是動作對變量取值的影響函數(shù).→i∶Loci×Cond(Var(oi))×Acti×Loci是條件遷移關(guān)系集合.Ooc0i?Loci是初始狀態(tài)集合.g0i∈Cond(Var(oi))是系統(tǒng)初始條件.

本文定義UML順序圖SD是由圖中所有對象在信道C上并發(fā)組成的一個信道系統(tǒng)(channel system，CS):

定義4 UML順序圖的信道系統(tǒng)語義.包含n個對象的順序圖是一個在(V，C)上由所有對象的程序圖并發(fā)組成信道系統(tǒng):CS(SD)=［PG1|…|PGn］，其中:V=U0≤i≤nVar(Oi).

根據(jù)模型檢測理論中信道系統(tǒng)與遷移系統(tǒng)的轉(zhuǎn)換關(guān)系定義UML順序圖的操作語義如下所示.

定義5 UML順序圖的操作語義.UML順序圖的操作語義是一個遷移系統(tǒng)TS(CS(SD))=(S，Act，→，I，AP，L)，

(li∈Loc0，i∧η|=g0，i)其中，η∈Eval(V)，ξ0表示信道的初始值為空.

L(＜ l1，…，ln，l，η，ξ＞ )={l1，…，ln|0 ＜ i≤n，li∈Loci}∪{g∈Cond(V)|η|=g}.

3 UML順序圖的自動驗證

3.1 UML 順序圖驗證過程

本文使用模型檢測器SPIN自動驗證UML順序圖描述的并發(fā)系統(tǒng)需求場景，具體流程如圖1所示.首先，用Rational Rose UML順序圖建模并發(fā)系統(tǒng)需求，導(dǎo)出由Rational Rose生成的順序圖的XML描述文件，使用自定義轉(zhuǎn)換規(guī)則將 XML文件轉(zhuǎn)換為Promela程序并將其加載到SPIN模型檢測器中，然后在SPIN中輸入描述系統(tǒng)規(guī)范的線性時序邏輯公式，運行SPIN執(zhí)行自動驗證，如果順序圖的Promela模型滿足規(guī)范，則檢測器返回TRUE，否則檢測器返回FALSE，并給出導(dǎo)致系統(tǒng)發(fā)生錯誤的運行跡以幫助修正模型.

圖1 順序圖驗證過程Fig.1 The validation process of sequence diagram

模型檢驗器SPIN是貝爾實驗室開發(fā)的一種模擬異步進程全部執(zhí)行過程的并發(fā)系統(tǒng)驗證工具.SPIN用類C語言Promela為系統(tǒng)建模，進程通過在消息通道上傳遞同步或異步消息實現(xiàn)進程之間通信，Promela核心語句的操作語義可由定義3中的程序圖定義，且所有并發(fā)進程的程序圖可組成定義4給出的信道系統(tǒng)，最后這個信道系統(tǒng)可以被轉(zhuǎn)換為遷移系統(tǒng)［18］，該遷移系統(tǒng)與定義5中的遷移系統(tǒng)同構(gòu).順序圖與Promela程序操作語義間的對應(yīng)關(guān)系為順序圖到Promela程序的自動轉(zhuǎn)換奠定了理論基礎(chǔ)，本文在后續(xù)的工作中根據(jù)二者的操作語義定義轉(zhuǎn)換規(guī)則，實現(xiàn)順序圖到Promela程序的轉(zhuǎn)換.3.2 UML順序圖到Promela的轉(zhuǎn)換過程

本文使用Rational Rose提供的Unisys插件獲取UML模型的XML描述文件，從中提取轉(zhuǎn)換過程所需的順序圖元素.UML順序圖的XML文件可被解析成一個樹狀結(jié)構(gòu)，如表1所示，樹的根節(jié)點主要包含2類子節(jié)點，一類子節(jié)點是圖中包含的并發(fā)對象節(jié)點，另一類子節(jié)點是圖中被傳遞的消息列表節(jié)點.并發(fā)對象節(jié)點包含若干屬性子節(jié)點，如:消息ID、消息發(fā)送者、消息接收者等，消息列表節(jié)點的子節(jié)點是消息節(jié)點，代表順序圖中的一條消息.消息節(jié)點包含若干屬性子節(jié)點，如:消息名，消息ID，消息類型等.

表1 順序圖XML文件的結(jié)構(gòu)Table 1 The structure of XML documents of Sequence diagrams

本文使用Java語言的DOM解析器解析順序圖的XML文件，讀取文檔結(jié)構(gòu)中各節(jié)點的信息以獲取轉(zhuǎn)換過程中需要的并發(fā)對象、消息列表、消息名、消息發(fā)送者、消息接收者、消息類型、消息序號等順序圖元素，算法偽代碼如下所示:

算法1 獲取UML順序圖的基本信息

輸入:順序圖的XML文件SD.xml

輸出:順序圖的基本信息類SDBaseInfo

1)創(chuàng)建順序圖基本信息類SDBaseInfo;

2)創(chuàng)建DOM解析工廠，通過工廠獲得DOM解析器;

3)解析SD.xml文件，返回Document對象;

4)獲取XML文件的根節(jié)點root及其子節(jié)點nodelist;

5)遍歷節(jié)點列表中的每個節(jié)點node，如果node是對象節(jié)點，則創(chuàng)建對象類ClassifierRole的實例cr，將node節(jié)點的所有屬性加入cr后，添加cr到順序圖基本信息類SDBaseInfo，如果node是消息列表節(jié)點，則將列表中的每個消息節(jié)點及其所有屬性添加到SDBaseInfo中;

6)返回順序圖基本信息類SDBaseInfo.

順序圖基本信息集到Promela語句的轉(zhuǎn)換規(guī)則如圖2所示.順序圖基本信息集中的對象被映射為Promela的進程語句，對象的屬性被映射為Promela進程的局部變量，消息類型被映射為Promela程序的消息通道類型，其他數(shù)據(jù)類型主要被映射為Promela程序的mtype類型.

圖2 轉(zhuǎn)換規(guī)則Fig.2 The conversion rules

表2 類圖XML文件的結(jié)構(gòu)Table 2 The structure of XML documents of class diagram

此外，為了實現(xiàn)Promela進程消息列表的自動獲取以及消息通道的自動生成，本文從順序圖中對象類圖的XML文件中提取附加信息，主要包括對象類構(gòu)造函數(shù)的參數(shù)列表以及對象類所包含的公共方法等基本信息，構(gòu)造函數(shù)參數(shù)列表映射為Promela語句的進程參數(shù)列表，公共方法名稱映射為Promela語句的進程通道名，公共方法的參數(shù)值映射為Promela語句的消息內(nèi)容.對象類圖的XML文檔結(jié)構(gòu)如表2所示，從XML文件中讀取類圖基本信息的方法與算法1類似.對于用模型檢測技術(shù)自動驗證UML順序圖，文獻［12］提出的實現(xiàn)方案與本文相似，本文所提方法與文獻［12］的不同之處在于:

首先，文獻［12］通過形式化定義UML順序圖直接給出順序圖基本元素到Promela語句的映射關(guān)系，而本文在順序圖操作語義與Promela核心語句操作語義同為遷移系統(tǒng)的理論基礎(chǔ)上定義順序圖基本元素到Promela語句的轉(zhuǎn)換規(guī)則，提高了轉(zhuǎn)換規(guī)則的合理性與正確性.

其次，文獻［12］通過分析UML順序圖的XML文件獲取轉(zhuǎn)換過程需要的基本信息.然而轉(zhuǎn)換過程中需要的部分信息如:對象的構(gòu)造函數(shù)以及公共方法等無法從順序圖的XML文件中直接獲取.本文根據(jù)UML順序圖中對象與類圖對象間的引用關(guān)系獲取上述信息，提高轉(zhuǎn)換過程的自動化程度.最后，在轉(zhuǎn)換規(guī)則的定義上，本文根據(jù)順序圖操作語義與Promela語義間的關(guān)系進行如下改進:

1)由一個對象連續(xù)發(fā)送或接受的消息被置于原子語句內(nèi).這樣做有2個優(yōu)點，首先，可以保證對象的消息在連續(xù)收發(fā)過程中不會被其他對象的消息交錯.其次，連續(xù)的消息收發(fā)過程中，每個語句會在Promela模型的狀態(tài)空間中生成一個狀態(tài)，而原子語句在模型狀態(tài)空間中只生成一個狀態(tài)，所以合理的使用原子語句可以縮小Promela模型的狀態(tài)空間，降低模型檢測過程的空間復(fù)雜度.

2)使用do循環(huán)語句內(nèi)嵌if條件語句建模并發(fā)消息列表.do循環(huán)語句與if語句的語義功能基本相同，二者間的主要差別在于，如果do循環(huán)語句中的選擇條件均未被滿足，本次循環(huán)體將被跳過，程序繼續(xù)執(zhí)行，當(dāng)if語句中的選擇條件均未被滿足時，Promela程序?qū)a(chǎn)生阻塞，直至有選擇條件被滿足，程序繼續(xù)執(zhí)行.使用do循環(huán)語句內(nèi)嵌if條件語句建模并發(fā)消息列表能夠充分描述并發(fā)消息隊列中消息收發(fā)活動的語義，這種語義僅用do循環(huán)語句描述是無法體現(xiàn)的，例如:如果一個對象的消息列表中沒有任何消息發(fā)送條件為真，那么此時該對象應(yīng)該產(chǎn)生阻塞狀態(tài)，直至有消息發(fā)送條件成立.

4 實例分析

本文以銀行ATM系統(tǒng)分布式并發(fā)設(shè)計［19］為例，用UML順序圖建模ATM系統(tǒng)驗證用戶輸入正確PIN過程的需求場景，如圖3所示，圖中的消息序列描述了自ATM客戶將ATM卡插入ATM讀卡器開始，至ATM系統(tǒng)成功驗證用戶輸入的正確PIN，向用戶顯示取款、查詢及轉(zhuǎn)賬選項菜單的過程.順序圖中各對象的類圖如圖4所示.

用本文提出的轉(zhuǎn)換方法得到ATM系統(tǒng)順序圖的Promela程序，如下所示:

圖3 ATM系統(tǒng)順序圖Fig.3 The sequence diagram of ATM system

圖4 ATM系統(tǒng)類圖集Fig.4 The class diagram set of ATM system

獲得ATM系統(tǒng)的Promela程序后啟動SPIN進行自動驗證，系統(tǒng)需求規(guī)范用線性時序邏輯(linear temporal logic，LTL)描述，例如，用戶輸入正確PIN后最終會向用戶顯示選項菜單menuIsShow，這個需求可以用LTL公式表示如下:

［］(p-＞ ＜ ＞ q)，其中命題符號p，q的預(yù)定 義 為:bool pin，bool menuIsShow，#definep(pin==true)，#define q(menuIsShow==true).運行SPIN執(zhí)行模型檢測，最終確認該順序圖場景滿足上述LTL公式.

對于另一個通信規(guī)范:更新用戶信息(消息14)應(yīng)發(fā)生在向用戶顯示選項菜單(消息15)之前，對應(yīng)的LTL公式表示如下:

［］(q-＞ p)，其中命題符號p，q的預(yù)定義為:bool updateStatuses，bool menuIsShow，#define p(updateStatuses = = true)， # define q(menuIsShow==true).

運行SPIN檢測上述LTL公式，生成的驗證結(jié)果如下，結(jié)果指出該系統(tǒng)模型不滿足LTL公式，并給出反例.

分析反例提供的系統(tǒng)錯誤運行跡，可發(fā)現(xiàn)產(chǎn)生錯誤的主要原因在于，雖然在順序圖的消息隊列中，消息14和15之間存在嚴(yán)格的發(fā)送順序，但是由于消息14和15之間不存在因果關(guān)系，所以二者屬于并發(fā)關(guān)系，導(dǎo)致在Promela程序中存在這樣一種運行跡，ATM事務(wù)系統(tǒng)還未及更新用戶信息，ATM用戶接口就已向用戶顯示選項菜單，即消息15的到達時間早于消息14，根據(jù)上述檢測結(jié)果，可以在順序圖中添加消息傳輸時間的約束信息，提示開發(fā)人員在后續(xù)設(shè)計階段避免此類錯誤的發(fā)生.

5 結(jié)束語

本文使用模型檢測技術(shù)自動驗證基于場景的并發(fā)系統(tǒng)需求設(shè)計，通過定義順序圖的操作語義建立順序圖到PROMELA程序的轉(zhuǎn)換規(guī)則，實現(xiàn)了轉(zhuǎn)換過程全部自動化，利用該方法可以降低驗證工作的難度，提高驗證效率，保證軟件開發(fā)過程的正確性.在下一步研究工作中，將繼續(xù)研究基于多個場景聯(lián)合驗證并發(fā)系統(tǒng)的需求設(shè)計，由于場景數(shù)量的增加，將導(dǎo)致遷移系統(tǒng)的狀態(tài)空間迅速膨脹，在模型檢測過程中產(chǎn)生狀態(tài)空間爆炸問題，所以提出有效的狀態(tài)空間縮減技術(shù)，避免狀態(tài)空間爆炸是未來的研究重點.

［1］LESCHER C.Global requirements engineering:decision support for globally distributed projects［C］//Proceedings of the 2009 Fourth IEEE International Conference on Global Software Engineering.Limerick，Ireland，2009.

［2］SONG I G，JEON S U，BAE D H.A graph based approach to detecting causes of implied scenarios under the asynchronous and synchronous communication styles［C］//Proceedings of 16th Asia-Pacific Software Engineering Conference.Penang，Malaysia，2009.

［3］朱雪峰，金芝.關(guān)于軟件需求中的不一致性管理［J］.軟件學(xué)報，2005，16(7):1221-1231.

ZHU Xuefeng，JIN Zhi.Managing the inconsistency of software requirements［J］.Journal of Software，2005，16(7):1221-1231.

［4］BREAUX T D，ANTóN A I，SPAFFORD E H.A distributed requirements management framework for legal compliance and accountability［J］.Computers ＆ Security，2009，28(1):8-17.

［5］BAXTER D，GAO J，CASE K，HARDING J，YOUNG B，COCHRANE S，DANI S.A framework to integrate design knowledge reuse and requirements management in engineering design［J］.Robotics and Computer-Integrated Manufacturing，2008，24(4):585-593.

［6］CLARKE E M，GRUMBERG O，PELED D A.Model checking［M］.Cambridge:MIT Press，1999:3-4.

［7］MCMILLAN L.Symbolic model checking［D］.Pitts burgh:Carnegie Mellon University，1992.

［8］HOLZMANN J.The model checker SPIN［J］.IEEE Trans on Software Engineering，1997，23(5):279-295.

［9］YAN F ，TANG T.Formal modeling and verification of realtime concurrent systems［C］//IEEE International Conference on Vehicular Electronics and Safety.Beijing，China，2007.

［10］TALUKDER K H，HARADA K.Message sequence charts to specify the communicating threads for concurrent discrete wavelet transform based image compression and a verification analysis［C］//Proceedings of Ninth ACIS International Conference on Software Engineering，Artificial Intelligence，Networking，and Parallel/Distributed Computing.Phuket，Thailand，2008.

［11］ALI Y，El-KASSAS S，MAHMOUD M.A rigorous methodology for security architecture modeling and verification［C］//Proceedings of the 42nd Annual Hawaii International Conference on System Sciences.Waikoloa，HI，United states，2009.

［12］王璐珍，董威，陳火旺，等.UML順序圖的自動驗證［J］.計算機工程與應(yīng)用，2003，39(29):80-83.

WANG Luzhen，DONG Wei，CHEN Huowang，et al.Automatic verification of UML sequence diagrams［J］.Computer Engineering and Applications，2003，39(29):80-83.

［13］KALIAPPAN P S，KOENIG H，KALIAPPAN V K.Designing and verifying communication protocols using model driven architecture and spin model checker［C］//Proceedings of 2008 International Conference on Computer Science and Software Engineering.Wuhan，China，2008.

［14］LI Jing，LI Jinhua，ZHANG Fangning.Model checking UML activity diagrams with SPIN［C］//Proceedings of International Conference on Computational Intelligence and Software Engineering.Wuhan，China，2009.

［15］SUTCLIFFER A.Scenario-based requirements engineering［C］//Proceedings of the 11th IEEE International Requirements Engineering Conference.Monterey，USA，2003.

［16］Object Management Group，OMG Unified Modeling Language Specification(Version 1.5)［s］.Framingham.2003.

［17］張巖，胡軍，于笑豐，等.場景驅(qū)動的構(gòu)件行為抽取［J］.軟件學(xué)報，2007，18(1):50-61.

ZHANG Yan，HU Jun，YU Xiaofeng，et al.Scenario-driven component behavior derivation［J］.Journal of Software，2007，18(1):50-61.

［18］CHRISTEL B，KATOEN J P，LARSEN K G.Principles of model checking［M］.Cambridge:The MIT Press，2008:30-60.

［19］GOMAA H.用UML設(shè)計并發(fā)、分布式、實時應(yīng)用［M］.呂慶中，譯.北京:北京航空航天大學(xué)出版社，2004:450-460.