基于場景的并發系統需求驗證方法研究

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

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

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

1 UML順序圖的形式化定義

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

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

2 UML順序圖的操作語義

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

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

S是系統狀態的有窮集合.Act是動作的有窮集合.→?S×Act×S表示遷移關系.I?S是系統初始狀態的有窮集合.AP是原子命題的有窮集合.L∶S→2AP是一個標簽函數.

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

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

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

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

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

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

根據模型檢測理論中信道系統與遷移系統的轉換關系定義UML順序圖的操作語義如下所示.

定義5 UML順序圖的操作語義.UML順序圖的操作語義是一個遷移系統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順序圖描述的并發系統需求場景，具體流程如圖1所示.首先，用Rational Rose UML順序圖建模并發系統需求，導出由Rational Rose生成的順序圖的XML描述文件，使用自定義轉換規則將 XML文件轉換為Promela程序并將其加載到SPIN模型檢測器中，然后在SPIN中輸入描述系統規范的線性時序邏輯公式，運行SPIN執行自動驗證，如果順序圖的Promela模型滿足規范，則檢測器返回TRUE，否則檢測器返回FALSE，并給出導致系統發生錯誤的運行跡以幫助修正模型.

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

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

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

表1 順序圖XML文件的結構Table 1 The structure of XML documents of Sequence diagrams

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

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

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

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

1)創建順序圖基本信息類SDBaseInfo;

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

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

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

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

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

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

圖2 轉換規則Fig.2 The conversion rules

表2 類圖XML文件的結構Table 2 The structure of XML documents of class diagram

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

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

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

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

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

4 實例分析

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

用本文提出的轉換方法得到ATM系統順序圖的Promela程序，如下所示:

圖3 ATM系統順序圖Fig.3 The sequence diagram of ATM system

圖4 ATM系統類圖集Fig.4 The class diagram set of ATM system

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

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

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

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

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

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

5 結束語

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

［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］朱雪峰，金芝.關于軟件需求中的不一致性管理［J］.軟件學報，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］.計算機工程與應用，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］張巖，胡軍，于笑豐，等.場景驅動的構件行為抽取［J］.軟件學報，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設計并發、分布式、實時應用［M］.呂慶中，譯.北京:北京航空航天大學出版社，2004:450-460.