基于場(chǎng)景的并發(fā)系統(tǒng)需求驗(yàn)證方法研究

張濤，黃少濱，黃宏濤，呂天陽(yáng)，劉剛

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

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

1 UML順序圖的形式化定義

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

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

2 UML順序圖的操作語(yǔ)義

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

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

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

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

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

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

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

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

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

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

定義5 UML順序圖的操作語(yǔ)義.UML順序圖的操作語(yǔ)義是一個(gè)遷移系統(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順序圖的自動(dòng)驗(yàn)證

3.1 UML 順序圖驗(yàn)證過(guò)程

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

圖1 順序圖驗(yàn)證過(guò)程Fig.1 The validation process of sequence diagram

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

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

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

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

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

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

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

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

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

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

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

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

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

順序圖基本信息集到Promela語(yǔ)句的轉(zhuǎn)換規(guī)則如圖2所示.順序圖基本信息集中的對(duì)象被映射為Promela的進(jìn)程語(yǔ)句，對(duì)象的屬性被映射為Promela進(jìn)程的局部變量，消息類型被映射為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

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

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

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

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

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

4 實(shí)例分析

本文以銀行ATM系統(tǒng)分布式并發(fā)設(shè)計(jì)［19］為例，用UML順序圖建模ATM系統(tǒng)驗(yàn)證用戶輸入正確PIN過(guò)程的需求場(chǎng)景，如圖3所示，圖中的消息序列描述了自ATM客戶將ATM卡插入ATM讀卡器開始，至ATM系統(tǒng)成功驗(yàn)證用戶輸入的正確PIN，向用戶顯示取款、查詢及轉(zhuǎn)賬選項(xiàng)菜單的過(guò)程.順序圖中各對(duì)象的類圖如圖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程序后啟動(dòng)SPIN進(jìn)行自動(dòng)驗(yàn)證，系統(tǒng)需求規(guī)范用線性時(shí)序邏輯(linear temporal logic，LTL)描述，例如，用戶輸入正確PIN后最終會(huì)向用戶顯示選項(xiàng)菜單menuIsShow，這個(gè)需求可以用LTL公式表示如下:

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

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

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

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

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

5 結(jié)束語(yǔ)

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

［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é)報(bào)，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順序圖的自動(dòng)驗(yàn)證［J］.計(jì)算機(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］張巖，胡軍，于笑豐，等.場(chǎng)景驅(qū)動(dòng)的構(gòu)件行為抽?。跩］.軟件學(xué)報(bào)，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è)計(jì)并發(fā)、分布式、實(shí)時(shí)應(yīng)用［M］.呂慶中，譯.北京:北京航空航天大學(xué)出版社，2004:450-460.