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

郭 兆，魏長江

(青島大學 數據科學與軟件工程學院，山東 青島 266071)

0 引 言

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

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

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

1 研究框架

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

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

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

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

模型檢驗階段：根據轉換成的形式模型和時態邏輯公式，利用NuSMV結構和語義上的關聯制定出轉換規則[5]，并把轉換后的模型利用模型檢驗工具檢測其中與屬性規約不一致的地方，得出滿足或者不滿足屬性規約的結論，為需求模型的完善提供關鍵性意見。

2 基于自然語言需求

2.1 需求子句相似度模型

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

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

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

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

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

Input: Requirement Description;

Output: Similar Sentence;

begin:

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

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

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

i=0,j=0; //設置變量i,j初始化

forall the Ai∈ RSido

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

newAi=n*Ai*Fi+n*Ai*N+T; //出現不規范詞用專業詞替換

forall the Fiin new Ando //重復遍歷每一個分詞處理結果

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++; //繼續循環

i++; //繼續循環

end;

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

(1)

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

假設有兩個需求描述子句見表1。

表1 需求相似度計算示例

以上需求子句經過分詞處理得：

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

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

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

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

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

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

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

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

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

圖3 簡單自動機模型

圖4 一個Event事件的狀態變遷

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

表2 具有分解規范的自然語言分解過程

使用以上表格分解規范時，需要施加規則。其中Action中的Agent表示代理，可以參與到一個或多個動作當中，是與系統交互的人或系統，是行為的執行者。Activity是人或者系統執行的操作，可能會導致狀態的改變，是行為本身。Object是受到原子動作中代理和資源作用影響的人或其它系統，是行為的被執行者。在電梯模型中，由于Action而導致整個系統的改變，開始時電梯在一樓，為空閑狀態，乘客進入電梯后,電梯由空閑變為待載，等待上行的指令。當乘客按下按鈕時，乘客作為代理操縱了系統，導致了系統狀態的改變，電梯由待載狀態變為上升狀態。根據上文提到的表格將具有分解規范的自然語言描述的需求分解成自動機模型如圖5所示。

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

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

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

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

在模型檢驗中，把系統的狀態變換等價為變量值的變化，變量值的改變體現了狀態的遷移，利用狀態間的約束關系和狀態轉移的關聯關系構成自動機模型或狀態圖[11]，因此在模型檢驗中使用上文的自動機模型可以將系統和待檢測的性質用同一種方式來表示。其檢驗過程如圖6所示。

圖6 模型檢驗過程

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

3.1 定 義

定義1 Kripke結構。令AP為原子命題集合，則AP上的Kripke結構M是一個三元組M=(S,R,L)， 其中，S是狀態的有限集合，R是完全變遷關系，L是標記函數，它標記在該狀態下為真的原子命題集合。

Kripke結構有向圖中，用圓圈表示可能的事件，有向弧線表示可能事件的關系，標記函數在圓圈內。

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

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

圖7 CTL公式結構

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

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

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

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

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

R(“Release”)表示從當前狀態開始到滿足第一個性質的狀態結束，第二個性質一直保持成立。

3.2 模型檢驗算法

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

圖8 房間加熱器的Kripke結構

因為結果集合中沒有包含初始狀態1，所以可以得出結論：這個用Kripke結構描述的系統不滿足給定的性質規約。

3.3 模型轉換與模型檢驗

采用模型檢驗方法需要對被測系統進行建模分析，用時序邏輯描述系統的結構和性質，利用模型內部的狀態遷移關系來驗證整個模型內部某些特定性質是否正確。本文用模型檢驗中的SMV語言描述描述待測系統，用CTL時態邏輯描述系統性質。對模型內部中系統狀態的可達性進行分析。

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

表3 自動機圖中元素與SMV的對應關系

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

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;

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

4 案例分析—電梯模型

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

4.1 電梯模型的描述與建模

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

上行：電梯初態停在一樓。當乘客按下上行按鈕后，電梯響應乘客的請求，向上運行。到達乘客所在樓層后，打開電梯門，乘客進入電梯，電梯檢測乘客重量是否超標。如果超重就報警，否則就關閉電梯門。然后乘客在電梯內按下目標樓層。電梯系統判斷目標樓層大于當前樓層，電梯向上運行。到達后乘客打開電梯門，乘客離開。電梯停在該樓層，并重新處于靜止狀態。

下行：當乘客按下下行按鈕后，電梯響應乘客的請求，向下運行。到達乘客所在樓層后，打開電梯門，乘客進入電梯，電梯檢測乘客重量是否超標。如果超重就報警，否則就關閉電梯門。然后乘客在電梯內按下目標樓層。電梯系統判定目標樓層小于當前樓層，電梯向下運行，到達后乘客打開電梯門，乘客離開。電梯停在該樓層，并重新處于靜止狀態。

報警：乘客在電梯內按下報警按鈕，或者電梯出現故障緊急停止后，報警。

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

開/關門：乘客在電梯內/外按下開/關門的按鈕后，電梯響應，打開或關閉電梯門。

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

表4 分詞提取后的結果

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

圖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的數據類型，為boolean型，第二處是weight,button_F1,button_F2,button_F3,door_F1,door_F2,door_F3,arrived的初始化描述。第三處省略的部分是對電梯狀態state和按鈕狀態door_F1,door_F2,door_F3的條件選擇結構。

4.2 屬性規約提取與驗證

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

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

表5 性質驗證結果

圖10 NuSMV驗證結果

狀態是否可達，結果顯示false，反例的出現說明了與預期不一致的行為，幫助構建更為完善的需求模型。④陷阱性質。結果顯示是false。表示能夠檢測出需求描述不一致的行為。反例的出現首先說明了能夠檢測出與描述不一致的行為，其次，根據反例提供的路徑信息可以進一步分析模型的內在聯系，幫助構建更為全面的需求模型。

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

5 結束語

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