基于模型檢驗的需求不一致研究

郭 兆，魏長江

(青島大學(xué) 數(shù)據(jù)科學(xué)與軟件工程學(xué)院，山東 青島 266071)

0 引 言

隨著計算機軟件自身規(guī)模的不斷增大和業(yè)務(wù)邏輯變得復(fù)雜，軟件需求在整個軟件開發(fā)中變得越來越重要。在軟件需求中，由于涉眾復(fù)雜，使用目前的一些建模與需求分析方法，還是不可避免帶來不一致性、不確定性等問題。其中，不一致的需求，會導(dǎo)致軟件系統(tǒng)的混亂，甚至是錯誤。因此，在需求分析階段，保證需求的一致性至關(guān)重要。

目前，解決需求一致性的方法主要分幾類：采用經(jīng)典邏輯檢測邏輯表達(dá)式的值來發(fā)現(xiàn)需求的不一致性[1]；采用模型檢驗的方法檢測需求規(guī)格說明中的錯誤；采用KAOS(knowledge acquisition in automated specification)方法通過建立具有自身語義的元模型發(fā)現(xiàn)矛盾。張建等[2]將UML(unified modeling language)模型集合轉(zhuǎn)化為時間自動機網(wǎng)絡(luò)模型并使用模型檢驗方法進(jìn)行驗證；周宇等[3]將層次自動機轉(zhuǎn)換為系統(tǒng)并發(fā)時間自動機使用模型檢驗方法進(jìn)行驗證，但是未能提供需求不一致的定位策略；李思杰等[4]結(jié)合SCR(soft cost reduction)方法和模型檢驗的方法進(jìn)行安全性和一致性驗證，但是過于形式化，不能保證其它參與者的理解。

為了獲得清晰且無二義性的軟件需求，又能保證用戶的理解，本文在現(xiàn)有研究基礎(chǔ)上提出一種基于自然語言描述與模型檢驗相結(jié)合的方法。該方法利用自然語言蘊含語義關(guān)系進(jìn)行提取并轉(zhuǎn)換成自動機模型，然后根據(jù)對應(yīng)關(guān)系轉(zhuǎn)換成相應(yīng)的形式模型并利用模型檢驗的工具和方法進(jìn)行一致性驗證。

1 研究框架

本文針對于需求分析中需求不一致的問題，提出了一種基于自然語言和模型檢驗相結(jié)合的需求描述分析方法。通過提取自然語言中的關(guān)鍵詞，建立自動機模型，利用模型間的關(guān)聯(lián)性將模型進(jìn)行轉(zhuǎn)換，將轉(zhuǎn)換后的模型和性質(zhì)規(guī)約引入模型檢驗中，通過模型檢驗發(fā)現(xiàn)不一致的需求。本文的研究框架圖如圖1所示,主要包含3部分內(nèi)容。

圖1 基于模型檢驗的需求不一致的研究框架

建模準(zhǔn)備階段：自然語言描述的需求有較強的表達(dá)能力，將自然語言描述的需求使用相似度算法計算出具有相似性的需求，給潛在的需求不一致提供定位策略。并使用模板提取需求語言中的關(guān)鍵詞。

模型建立階段：提取自然語言中的關(guān)鍵詞后，使用表格轉(zhuǎn)換法轉(zhuǎn)換成自動機模型，并利用模型間的關(guān)聯(lián)性轉(zhuǎn)換成能被模型檢驗識別的形式模型(SMV模型)。同時在轉(zhuǎn)換過程中，對屬性進(jìn)行說明，將屬性規(guī)約用計算樹邏輯(computaiton tree logic,CTL)進(jìn)行描述。

模型檢驗階段：根據(jù)轉(zhuǎn)換成的形式模型和時態(tài)邏輯公式，利用NuSMV結(jié)構(gòu)和語義上的關(guān)聯(lián)制定出轉(zhuǎn)換規(guī)則[5]，并把轉(zhuǎn)換后的模型利用模型檢驗工具檢測其中與屬性規(guī)約不一致的地方，得出滿足或者不滿足屬性規(guī)約的結(jié)論，為需求模型的完善提供關(guān)鍵性意見。

2 基于自然語言需求

2.1 需求子句相似度模型

在需求分析過程中，表達(dá)能力較強的自然語言常用于需求描述，不同參與者從不同角度描述的需求不可避免存在重復(fù)現(xiàn)象，Spanoudakis認(rèn)為兩個需求描述元素之間存在重疊關(guān)系，重疊關(guān)系有4種，包含無重疊關(guān)系、完全重疊關(guān)系、包含性重疊關(guān)系和部分重疊關(guān)系，當(dāng)重疊關(guān)系出現(xiàn)后3種的時候，才可能會導(dǎo)致需求描述的不一致性的現(xiàn)象發(fā)生，可以說需求重疊現(xiàn)象是出現(xiàn)需求不一致的根本原因?？紤]到需求描述重疊的情況，本文提出使用相似度方法計算自然語言描述需求，若兩個自然語言的需求描述相似度越高說明重疊概率越大，即存在需求不一致的概率越大。

本文以自然語言需求子句為結(jié)點，構(gòu)建了一種需求子句模型。如圖2所示，使用句子相似度算法，表征句子之間的相似性。

圖2 由自然語言生成的需求子句模型

在處理過程中，將自然語言描述的需求劃分為需求子句(sentence)，然后對需求子句進(jìn)行分詞處理,統(tǒng)計每個需求子句中詞語的詞頻(F)和詞性(N),利用相似度算法計算出這些需求子句的相似度，把具有相似度需求子句放到一個組里。其中,詞頻(F)表示需求子句中某個關(guān)鍵詞出現(xiàn)次數(shù)的統(tǒng)計量，初始值為1，隨著不斷切詞累增。詞性(N),是一組枚舉值，取值范圍{n,v,adj,adv,nq,pro,pre,con}分別表示名詞、動詞、形容詞、副詞、數(shù)量詞、代詞、介詞、連接詞,為了解決部分詞語不規(guī)范的問題，使用可替換同義詞(T)表示需求領(lǐng)域內(nèi)對某些名詞的通用規(guī)范用法。算法1給出了需求子句相似度的計算過程，相應(yīng)的算法偽代碼表示如下：

算法1： 需求子句相似度算法

Input: Requirement Description;

Output: Similar Sentence;

begin:

Requirement Description(DS)?； //需求描述

Requirement Sentence(RS) ∈?； //需求子句為空

n* RS ← DS； //將需求描述轉(zhuǎn)換為n個需求子句

i=0,j=0; //設(shè)置變量i,j初始化

forall the Ai∈ RSido

n*Ai*Fi+n*Ai*N =RSidivided; //遍歷所有子句， 將子句進(jìn)行分詞處理， 劃分成詞頻和詞性

newAi=n*Ai*Fi+n*Ai*N+T; //出現(xiàn)不規(guī)范詞用專業(yè)詞替換

forall the Fiin new Ando //重復(fù)遍歷每一個分詞處理結(jié)果

j=i；

forall the Fjin new An/2do //任意兩個之間作比較

j=i;

if(SimFreq(Fj,new An/2)>0.5) //相似度大于0.5

then

add Fj∪new An/2join Similar Sentence[ ]//相似的放在一組

n++; //繼續(xù)循環(huán)

i++; //繼續(xù)循環(huán)

end;

需求描述里的關(guān)鍵詞信息能夠直觀反應(yīng)關(guān)鍵詞在文本中的重要程度[6]，當(dāng)關(guān)鍵詞在文檔中出現(xiàn)的次數(shù)越多，說明該詞所占比例越大即所占的權(quán)重越高。本文借鑒于傳統(tǒng)的VSM[7]計算方法，基于向量空間模型的算法，使用兩個向量的夾角表示出兩個向量之間的相似度。其計算過程如式(1)所示

(1)

通過式(1)來計算兩個需求子句之間的相似度, 首先根據(jù)上文提到的需求子句進(jìn)行分詞處理，然后進(jìn)行詞頻計算并形成特征向量，這樣可以將兩個需求子句這種非結(jié)構(gòu)化數(shù)據(jù)抽象為向量表現(xiàn)形式, 之后便可以將自然語言表述的需求問題轉(zhuǎn)換成數(shù)學(xué)上的向量夾角問題，同時需求關(guān)鍵詞詞頻的數(shù)量在一定程度上能夠反映重要程度，當(dāng)需求描述文本規(guī)模比較大時，使用此方法可以有效且快速找出需求相似的地方，為解決需求不一致提供定位策略。示例過程如下所示：

假設(shè)有兩個需求描述子句見表1。

表1 需求相似度計算示例

以上需求子句經(jīng)過分詞處理得：

需求子句1:“乘客 按下 向上 按鈕 電梯 響應(yīng) 請求 向上運行”

需求子句2:“乘客 按下 向下 按鈕 電梯 響應(yīng) 請求 向下運行”

獲得向量集 “乘客 按下 向上 向下 按鈕電梯 響應(yīng) 請求 向上運行 向下運行”

對于需求子句A:乘客(1)按下(1)向上(1)向下(0)按鈕(1)電梯(1)響應(yīng)(1)請求(1)向上運行(1)向下運行(0)。

對于需求子句B:乘客(1)按下(1)向上(0)向下(1)按鈕(1)電梯(1)響應(yīng)(1)請求(1)向上運行(0)向下運行(1)。

經(jīng)過詞頻計算得A需求子句的特征向量 {1,1,1,0,1,1,1,1,1,0}， B需求子句的特征向量 {1,1,0,1,1,1,1,1,0,1}。 根據(jù)式(1)計算得兩個需求子句的相似度為2/3，說明兩句需求描述的語句比較相似，根據(jù)需求重疊理論，需求越相似的地方存在不一致的概率越大,所以首先定位到這兩句需求描述的位置，以這兩句為基礎(chǔ)結(jié)合上下文進(jìn)行建模分析。

2.2 需求子句提取自動機模型

自動機是有限狀態(tài)機(FSM)的數(shù)學(xué)模型, 是表示有限個狀態(tài)以及在這些狀態(tài)之間的轉(zhuǎn)移和動作等行為的模型。有限狀態(tài)機是一個五元組： (Σ,Q,Δ,q0,F)， 其中：Σ是一個有限字母表。 Q是一個有限狀態(tài)集合。 Δ?Q×Σ→Q代表變遷關(guān)系。q0?Q是起始狀態(tài)。 F?Q是終止?fàn)顟B(tài)的集合。

自動機可以用于并發(fā)系統(tǒng)和交互式系統(tǒng)建模。一個簡單的自動機模型如圖3所示，q0表示系統(tǒng)的起始狀態(tài)，q2和q3是終止?fàn)顟B(tài)F，q1是過程狀態(tài)，它們都屬于狀態(tài)集合Q， 其余為狀態(tài)變遷。狀態(tài)Q和字母表Σ都可以表示待建模系統(tǒng)狀態(tài)的集合。本節(jié)中，將需求定義為一組由動作序列控制的狀態(tài)變遷關(guān)系[8]，以此刻畫自動機模型,將具有分解規(guī)范的自然語言指定為由事件(Event)、狀態(tài)(State)以及動作列表(Action)組成的結(jié)構(gòu)。這種類型的規(guī)范結(jié)構(gòu)描述了一個由動作和事件驅(qū)動的狀態(tài)改變結(jié)構(gòu)。其中，Event 是指導(dǎo)致系統(tǒng)表現(xiàn)出可預(yù)測行為的動作或過程。State表示某時刻系統(tǒng)的某個行為。Action表示人或系統(tǒng)的操作列表，可能會導(dǎo)致狀態(tài)的改變。一個簡單的狀態(tài)變遷如圖4所示。

圖3 簡單自動機模型

圖4 一個Event事件的狀態(tài)變遷

本文結(jié)合此方法和BDL方法[9]對模型進(jìn)行改進(jìn)，改進(jìn)后的表述使用電梯模型描述此行為，見表2.

表2 具有分解規(guī)范的自然語言分解過程

使用以上表格分解規(guī)范時，需要施加規(guī)則。其中Action中的Agent表示代理，可以參與到一個或多個動作當(dāng)中，是與系統(tǒng)交互的人或系統(tǒng)，是行為的執(zhí)行者。Activity是人或者系統(tǒng)執(zhí)行的操作，可能會導(dǎo)致狀態(tài)的改變，是行為本身。Object是受到原子動作中代理和資源作用影響的人或其它系統(tǒng)，是行為的被執(zhí)行者。在電梯模型中，由于Action而導(dǎo)致整個系統(tǒng)的改變，開始時電梯在一樓，為空閑狀態(tài)，乘客進(jìn)入電梯后,電梯由空閑變?yōu)榇d，等待上行的指令。當(dāng)乘客按下按鈕時，乘客作為代理操縱了系統(tǒng)，導(dǎo)致了系統(tǒng)狀態(tài)的改變，電梯由待載狀態(tài)變?yōu)樯仙隣顟B(tài)。根據(jù)上文提到的表格將具有分解規(guī)范的自然語言描述的需求分解成自動機模型如圖5所示。

圖5 電梯空閑事件的自動機模型

圖5描述了由自然語言過渡到自動機模型的一個例子，從圖中可以看出，由于整個的Action行為才導(dǎo)致系統(tǒng)狀態(tài)的變遷，這符合BDL中描述的行為執(zhí)行者依照軟件功能對被執(zhí)行者實施操作的過程。

3 基于模型檢驗的一致性驗證

模型檢驗最早是由Clarke和Emerson以及Quielle和Sikakis在針對時態(tài)邏輯實際驗證算法時提出。目前在系統(tǒng)的安全性和一致性方面應(yīng)用很廣[10],模型檢驗是一種自動驗證系統(tǒng)模型是否具有特定性質(zhì)的方法，簡單來說就是先把系統(tǒng)建模為有限狀態(tài)轉(zhuǎn)移系統(tǒng)，后利用時態(tài)邏輯描述待驗證的規(guī)范，對整個系統(tǒng)的行為空間進(jìn)行自動化遍歷搜索，與定理證明按照一步步展開嚴(yán)格證明推導(dǎo)不同，模型檢驗具有自動化和高效化的特點。

在模型檢驗中，把系統(tǒng)的狀態(tài)變換等價為變量值的變化，變量值的改變體現(xiàn)了狀態(tài)的遷移，利用狀態(tài)間的約束關(guān)系和狀態(tài)轉(zhuǎn)移的關(guān)聯(lián)關(guān)系構(gòu)成自動機模型或狀態(tài)圖[11]，因此在模型檢驗中使用上文的自動機模型可以將系統(tǒng)和待檢測的性質(zhì)用同一種方式來表示。其檢驗過程如圖6所示。

圖6 模型檢驗過程

本文將需求描述的系統(tǒng)模型的自動機圖，轉(zhuǎn)化為一個模型檢驗的問題，即將自然語言描述的需求問題，轉(zhuǎn)換模型檢驗中的“狀態(tài)不可達(dá)”，“不存在此條路徑”等類似性質(zhì)進(jìn)行驗證[12]。通過建立被測系統(tǒng)的狀態(tài)行為模型，并用CTL時態(tài)邏輯描述系統(tǒng)待驗證的性質(zhì)，經(jīng)由模型檢驗工具NuSMV檢測，最終得出一條反例。反例的出現(xiàn)首先表明性質(zhì)規(guī)約驗證了模型，其次反例的出現(xiàn)可以加大對模型的理解，發(fā)現(xiàn)模型的不足?；诖耍黾訉δＰ偷尿炞C部分，包括可達(dá)性，前向一致性，陷阱性質(zhì)的驗證。其中，可達(dá)性的表述為在一次狀態(tài)變換中，總是至少存在一條路徑可以到達(dá)目標(biāo)狀態(tài)。前向一致性的表述為如果某個狀態(tài)S1出現(xiàn)，那么該系統(tǒng)模型在后續(xù)變換中一定能夠出現(xiàn)可預(yù)見的狀態(tài)S2。例如，事件S1表示電梯系統(tǒng)啟動，事件S2表示乘客按下上行按鈕，事件S3表示電梯到達(dá)目標(biāo)樓層。則事件S1和事件S2滿足前向一致性。陷阱性質(zhì)的描述為對某一性質(zhì)進(jìn)行取反操作，由模型檢驗的工具進(jìn)行檢測。通過檢測以上性質(zhì)可以得出和預(yù)期不一致的地方，并通過產(chǎn)生的反例幫助構(gòu)建更為完整的需求模型。

3.1 定 義

定義1 Kripke結(jié)構(gòu)。令A(yù)P為原子命題集合，則AP上的Kripke結(jié)構(gòu)M是一個三元組M=(S,R,L)， 其中，S是狀態(tài)的有限集合，R是完全變遷關(guān)系，L是標(biāo)記函數(shù)，它標(biāo)記在該狀態(tài)下為真的原子命題集合。

Kripke結(jié)構(gòu)有向圖中，用圓圈表示可能的事件，有向弧線表示可能事件的關(guān)系，標(biāo)記函數(shù)在圓圈內(nèi)。

定義2 計算樹邏輯(CTL*)。是一種離散、分支時間、命題時態(tài)邏輯，將系統(tǒng)的狀態(tài)變化的所有可能性表示為樹狀結(jié)構(gòu)。

計算樹邏輯的語法結(jié)構(gòu)如下：CTL*式由路徑量詞和時序運算符組成。路徑量詞的作用是表述計算樹邏輯的結(jié)構(gòu)，由A和E兩種構(gòu)成,如圖7所示。

圖7 CTL公式結(jié)構(gòu)

A表示從當(dāng)前開始在未來的所有路徑符合某一性質(zhì)。E表示從當(dāng)前開始在未來至少有一條路徑符合性質(zhì)。有5個基本的運算符，直觀上的意義如下：

X(“Next”)說明從某狀態(tài)起始路徑的第二個狀態(tài)開始，性質(zhì)滿足。

F(“Finally”)刻畫從路徑中的某個狀態(tài)開始，最終性質(zhì)滿足。

G(“Global”)說明性質(zhì)在路徑上的每個狀態(tài)都滿足。

U(“Until”)表示在此狀態(tài)之前路徑上所有狀態(tài)第一性質(zhì)滿足。

R(“Release”)表示從當(dāng)前狀態(tài)開始到滿足第一個性質(zhì)的狀態(tài)結(jié)束，第二個性質(zhì)一直保持成立。

3.2 模型檢驗算法

本文以一個簡單的例子來說明模型檢驗算法。例如：房間加熱器可能處于如下的4種狀態(tài)中的任何一個：Idle——空閑狀態(tài)；End——結(jié)束使用；Heat——開始加熱，達(dá)到某個溫度；Warning——系統(tǒng)警告。圖8給出了房間加熱器Kripke結(jié)構(gòu)。為清楚起見，每個狀態(tài)都用在該狀態(tài)為真的原子命題和在該狀態(tài)為假的原子命題的否定形式標(biāo)記出來，帶箭頭的弧標(biāo)記表示了引起狀態(tài)變遷的動作名稱。

圖8 房間加熱器的Kripke結(jié)構(gòu)

因為結(jié)果集合中沒有包含初始狀態(tài)1，所以可以得出結(jié)論：這個用Kripke結(jié)構(gòu)描述的系統(tǒng)不滿足給定的性質(zhì)規(guī)約。

3.3 模型轉(zhuǎn)換與模型檢驗

采用模型檢驗方法需要對被測系統(tǒng)進(jìn)行建模分析，用時序邏輯描述系統(tǒng)的結(jié)構(gòu)和性質(zhì)，利用模型內(nèi)部的狀態(tài)遷移關(guān)系來驗證整個模型內(nèi)部某些特定性質(zhì)是否正確。本文用模型檢驗中的SMV語言描述描述待測系統(tǒng)，用CTL時態(tài)邏輯描述系統(tǒng)性質(zhì)。對模型內(nèi)部中系統(tǒng)狀態(tài)的可達(dá)性進(jìn)行分析。

將上文提到的自動機圖提取狀態(tài)元素轉(zhuǎn)換成SMV模型，以供模型檢驗的工具所識別。SMV模型包含變量聲明模塊VAR和IVAR，關(guān)鍵字定義模塊MOUDLE；使用ASSIGN模塊定義系統(tǒng)的初始狀態(tài)，使用INIT定義系統(tǒng)初始狀態(tài)的變量值。其對應(yīng)轉(zhuǎn)換規(guī)則見表3。

表3 自動機圖中元素與SMV的對應(yīng)關(guān)系

按照表3的描述，可以將上文中的自動機圖用SMV的語法表達(dá)出來。如下所示:

MOUDULE main

VAR

state：{IDLE,UP,DOWN}

button_F1:boolean

ASSIGN:

init(state):IDLE;

init(button_F1):false;

next(state):case

state:IDLE&button_F1:UP

esac;

可以看出，提取出圖中元素后按照對應(yīng)關(guān)系可以將上文提到的自動機模型逐步轉(zhuǎn)換成能被模型檢驗工具所識別的SMV模型。

4 案例分析—電梯模型

由于完整的系統(tǒng)模型龐大而復(fù)雜，本文通過精簡電梯模型[13]，選取電梯模型對上述研究方法進(jìn)行驗證。

4.1 電梯模型的描述與建模

電梯的功能分為上行、下行、報警、顯示、開/關(guān)門、電話機報警等。該模型的部分自然語言描述如下：

上行：電梯初態(tài)停在一樓。當(dāng)乘客按下上行按鈕后，電梯響應(yīng)乘客的請求，向上運行。到達(dá)乘客所在樓層后，打開電梯門，乘客進(jìn)入電梯，電梯檢測乘客重量是否超標(biāo)。如果超重就報警，否則就關(guān)閉電梯門。然后乘客在電梯內(nèi)按下目標(biāo)樓層。電梯系統(tǒng)判斷目標(biāo)樓層大于當(dāng)前樓層，電梯向上運行。到達(dá)后乘客打開電梯門，乘客離開。電梯停在該樓層，并重新處于靜止?fàn)顟B(tài)。

下行：當(dāng)乘客按下下行按鈕后，電梯響應(yīng)乘客的請求，向下運行。到達(dá)乘客所在樓層后，打開電梯門，乘客進(jìn)入電梯，電梯檢測乘客重量是否超標(biāo)。如果超重就報警，否則就關(guān)閉電梯門。然后乘客在電梯內(nèi)按下目標(biāo)樓層。電梯系統(tǒng)判定目標(biāo)樓層小于當(dāng)前樓層，電梯向下運行，到達(dá)后乘客打開電梯門，乘客離開。電梯停在該樓層，并重新處于靜止?fàn)顟B(tài)。

報警：乘客在電梯內(nèi)按下報警按鈕，或者電梯出現(xiàn)故障緊急停止后，報警。

顯示：顯示面板會一直顯示電梯的狀態(tài)(運行狀態(tài)、當(dāng)前所在樓層)；如果發(fā)生故障或者乘客按下報警按鈕，顯示面板顯示為“不可用”。

開/關(guān)門：乘客在電梯內(nèi)/外按下開/關(guān)門的按鈕后，電梯響應(yīng)，打開或關(guān)閉電梯門。

對以上自然語言使用2.1節(jié)中的相似度算法進(jìn)行分析，得到描述上行和下行需求描述的相似度約為0.95，說明兩個需求描述存在重疊的地方，所以定位到這兩個需求描述的位置，以此位置開始進(jìn)行建模分析，避免遇到大規(guī)模的需求描述無法快速找到潛在不一致需求的情況。發(fā)現(xiàn)具有相似性需求描述后，根據(jù)2.2節(jié)中的分解規(guī)范提取自動機模型，其分解過程見表4。

表4 分詞提取后的結(jié)果

根據(jù)表格提示結(jié)合上下文補充必要的節(jié)點可以生成自動機模型，為了便于觀察，轉(zhuǎn)換成自動機形式，如圖9所示。根據(jù)表3的方法結(jié)合圖6，可以簡單生成一個電梯系統(tǒng)的SMV模型，該模型表述如下所示：(由于篇幅有限，只選取部分關(guān)鍵代碼)。

圖9 電梯模型的自動機模型

MODULE main

VAR

state:{Up,Down,Hold,Idle,Waiting,Warning,Stop,Fault};

position:{F1,F2,F3};

button_F1:boolean;

……

door_F1:{Opening,Opened,Closing,Closed};

door_F2:{Opening,Opened,Closing,Closed};

door_F3:{Opening,Opened,Closing,Closed};

passenger:{None,In,Out};

weight:{None,Normal,Overload};

arrived:boolean;

emergency:boolean;

ASSIGN

init(state)：= Idle;

init(passenger):=None;

……

next(position):=case

position=F1&state=Up:F2;

position=F2&state=Up:F3;

position=F2&state=Down:F1;

position=F3&state=Down:F2;

door_F1=Closed&(!button_F1)&position=F1

&state=Up:F2;

door_F3=Closed&(!button_F3)&position=F3

&state=Down:F2;

door_F2=Closed&(!button_F2)&position=F2

&state=Up:F3;

door_F2=Closed&(!button_F2)&position=F2

&state=Down:F1;

TRUE:position;

esac;

next(state):= case

state=Idle&(door_F1=Opening&passenger=In

&weight=Normal): Waiting;

state=Idle&(passenger=In&weight=Overload):

Warning;

state=Waiting&(passenger=In&weight=Normal&(button_F2|button_F3)): Up;

state=Waiting&(passenger=In&weight=Normal&

button_F1|button_F2): Down;

state=Waiting&emergency:Stop;

……

esac;

上述代碼是對電梯模型的一個描述，代碼中有幾處省略部分，其中第一處是button_F2,button_F3,request_F1,request_F2,request_F3的數(shù)據(jù)類型，為boolean型，第二處是weight,button_F1,button_F2,button_F3,door_F1,door_F2,door_F3,arrived的初始化描述。第三處省略的部分是對電梯狀態(tài)state和按鈕狀態(tài)door_F1,door_F2,door_F3的條件選擇結(jié)構(gòu)。

4.2 屬性規(guī)約提取與驗證

屬性規(guī)約是系統(tǒng)運行過程中必須滿足的規(guī)范，其保證了系統(tǒng)的一致性和安全性。針對于本文提到模型，主要從以下幾個方面進(jìn)行驗證：①安全性。一個系統(tǒng)的運行首先要保證其安全性，對此要驗證的是：在未來的任意一個時刻，電梯系統(tǒng)都不會把乘客困在電梯中。②前向一致性。電梯系統(tǒng)的運行需要滿足前向一致性。對此驗證電梯初始狀態(tài)為空閑狀態(tài)時，當(dāng)有乘客進(jìn)入時，未來的某一狀態(tài)會由于超重導(dǎo)致電梯報警。③可達(dá)性。對此要驗證電梯系統(tǒng)的自動機模型是否可以到達(dá)任何一個圖中描述的狀態(tài)。④陷阱性質(zhì)。根據(jù)自動機圖中描述的狀態(tài)變遷，人為增加一條和某一行為需求描述相似的變遷，對其進(jìn)行取反操作，觀察模型檢驗?zāi)芊駲z測出相似且不一致的行為。對此要驗證當(dāng)有乘客在一樓且按下上行按鈕后，電梯不會出現(xiàn)上行狀態(tài)。檢測結(jié)果見表5。

表5是對以上幾個屬性規(guī)約性的表述。圖10是NuSMV的驗證結(jié)果。下面對NuSMV的驗證結(jié)果進(jìn)行分析。①安全性的CTL描述是在所有正常情況中，乘客不能被困在電梯中，結(jié)果顯示是true，驗證該電梯模型具有安全性質(zhì)。②前向一致性。結(jié)果顯示是true。表示在模型轉(zhuǎn)換過程中狀態(tài)前后的變遷關(guān)系是正確的，說明按照本文的轉(zhuǎn)換規(guī)則從自然語言轉(zhuǎn)換的自動機模型是可信的。③可達(dá)性的表述為，按照需求定義的功能判斷整個系統(tǒng)中的某個

表5 性質(zhì)驗證結(jié)果

圖10 NuSMV驗證結(jié)果

狀態(tài)是否可達(dá)，結(jié)果顯示false，反例的出現(xiàn)說明了與預(yù)期不一致的行為，幫助構(gòu)建更為完善的需求模型。④陷阱性質(zhì)。結(jié)果顯示是false。表示能夠檢測出需求描述不一致的行為。反例的出現(xiàn)首先說明了能夠檢測出與描述不一致的行為，其次，根據(jù)反例提供的路徑信息可以進(jìn)一步分析模型的內(nèi)在聯(lián)系，幫助構(gòu)建更為全面的需求模型。

事實上，當(dāng)變換面臨的狀態(tài)越多時，則所需要遍歷的路徑也就越多，不僅工作量大，而且容易忽略一些狀態(tài)變換；而模型檢驗可以自動遍歷所有狀態(tài)，遇到與預(yù)期性質(zhì)不一致的情況時自動生成一條反例。通過分析反例得出通過自然語言建立的模型的不足之處，以供繼續(xù)分析完善模型。另一方面，當(dāng)模型的狀態(tài)空間變得足夠大時，人工的方法幾乎已經(jīng)無法解決狀態(tài)的遍歷問題，只能依靠自動或者半自動的方法，這也是模型檢驗的優(yōu)勢所在。

5 結(jié)束語

針對于需求分析階段難以獲得清晰且一致性需求，本文提出一種使用自然語言和模型檢驗相結(jié)合的方法，使用相似度算法解決需求不一致定位問題，后進(jìn)行模型提取和轉(zhuǎn)換，并使用模型檢驗的方法進(jìn)行驗證和分析。最后通過電梯系統(tǒng)模型進(jìn)行驗證。結(jié)果表明，本文提到的方法有效，有助于對復(fù)雜系統(tǒng)的建模分析和測試。今后將繼續(xù)對此方法進(jìn)行研究，使其具有更高的普遍性并側(cè)重于開發(fā)一套完整的工具集，便于更好的分析和驗證。