基于模型檢驗(yàn)的需求不一致研究

郭 兆，魏長(zhǎng)江

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

0 引 言

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

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

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

1 研究框架

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

圖1 基于模型檢驗(yàn)的需求不一致的研究框架

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

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

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

2 基于自然語(yǔ)言需求

2.1 需求子句相似度模型

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

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

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

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

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

Input: Requirement Description;

Output: Similar Sentence;

begin:

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

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

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

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ù)遍歷每一個(gè)分詞處理結(jié)果

j=i；

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

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ù)越多，說(shuō)明該詞所占比例越大即所占的權(quán)重越高。本文借鑒于傳統(tǒng)的VSM[7]計(jì)算方法，基于向量空間模型的算法，使用兩個(gè)向量的夾角表示出兩個(gè)向量之間的相似度。其計(jì)算過(guò)程如式(1)所示

(1)

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

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

表1 需求相似度計(jì)算示例

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

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

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

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

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

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

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

2.2 需求子句提取自動(dòng)機(jī)模型

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

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

圖3 簡(jiǎn)單自動(dòng)機(jī)模型

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

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

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

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

圖5 電梯空閑事件的自動(dòng)機(jī)模型

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

3 基于模型檢驗(yàn)的一致性驗(yàn)證

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

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

圖6 模型檢驗(yàn)過(guò)程

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

3.1 定 義

定義1 Kripke結(jié)構(gòu)。令A(yù)P為原子命題集合，則AP上的Kripke結(jié)構(gòu)M是一個(gè)三元組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 計(jì)算樹(shù)邏輯(CTL*)。是一種離散、分支時(shí)間、命題時(shí)態(tài)邏輯，將系統(tǒng)的狀態(tài)變化的所有可能性表示為樹(shù)狀結(jié)構(gòu)。

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

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

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

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

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

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

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

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

3.2 模型檢驗(yàn)算法

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

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

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

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

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

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

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

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

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;

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

4 案例分析—電梯模型

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

4.1 電梯模型的描述與建模

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

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

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

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

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

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

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

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

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

圖9 電梯模型的自動(dòng)機(jī)模型

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;

上述代碼是對(duì)電梯模型的一個(gè)描述，代碼中有幾處省略部分，其中第一處是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的初始化描述。第三處省略的部分是對(duì)電梯狀態(tài)state和按鈕狀態(tài)door_F1,door_F2,door_F3的條件選擇結(jié)構(gòu)。

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

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

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

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

圖10 NuSMV驗(yàn)證結(jié)果

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

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

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

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