面向模型檢測的LTL語句自動生成方法

段喜龍，陸智偉+，鄭 巍，陳晉升，樊 鑫，肖 鵬

(1.南昌航空大學 軟件學院，江西 南昌 330063；2.南昌航空大學 軟件測評中心，江西 南昌 330063)

0 引 言

模型檢測作為軟件系統驗證中的一個常用手段，已經在多個領域得到了應用。在基于模型開發的軟件系統驗證中，線性時態邏輯LTL(linear-time temporal logic)用于描述軟件的性質，這些性質又被稱為線性時間屬性。這是邁向構建模型檢測理論重要的一步，現已得到了廣泛的應用[1-4]。

LTL能得到廣泛應用有賴于人們對它的表達能力的研究。文獻[5]中給出，LTL的表達能力與一階謂詞邏輯等價。盡管它們的表達能力是一樣的，但兩者在可滿足性問題，可判定問題還有推理問題上的解決難易程度卻大不相同。這些問題在一階謂詞邏輯上的解決難度是非初等的，也就是說它的解決方案的復雜度上界是可以無限增長的[6，7]。而在LTL上，這些問題的解決難度都只是PSPACE-完全的[8，9]。這也是能夠得到廣泛應用的一個重要的理論支撐。而LTL語句生成需要測試人員對被測模型要有充分的了解，而這一過程需要花費很多時間。

在模型檢測方面，文獻[12]從時間邏輯角度對系統行為進行了刻畫，文獻[13]采用時間抽象互模擬方法來驗證模型；文獻[14]分別采用動態層次化UML狀態機模型和符號模型進行驗證；文獻[15]將時間自動機(timed automata，TA)模型轉換為有限狀態遷移圖，并將有限狀態遷移圖轉換為非確定有限狀態機(finite state machine，FSM)，從而采用基于FSM的方法進行測試；文獻[16]是一種通過在運行時驗證軟件源代碼中的斷言來檢測不一致的方法。但是這些工作都不是完全自動化的，驗證人員需要手動的生成LTL語句，驗證效率低。因此，研究和實現LTL自動生成的方法是必要的。

本文提出了一個基于自然語言處理的線性時態邏輯自動生成的方法，支持基于模型的開發軟件設計的分析。在本文的方法中，通過自動生成線性時態邏輯聲明來建立來對模型與需求的進行一致性分析。本文研究的目標是減少在軟件開發后期檢測需求模型一致性所需的工作。

1 本文工作

本文提出的LTL語句自動生成方法如圖1所示。本文采用的輸入是需求說明書和UML模型，然后采用關鍵詞提取，基于注釋UML模型的LTL生成方法，從而生成LTL語句。

圖1 LTL語句自動生成方法

1.1 關鍵詞提取

關鍵詞提取是本文根據需求文檔生成LTL驗證語句的關鍵步驟。關鍵詞提取流程如圖2所示，首先對需求文檔進行分詞，采用語言技術平臺(language technology plantform，LTP)[17]，LTP提供了一系列中文自然語言處理工具，用戶可以使用這些工具對于中文文本進行分詞、詞性標注、句法分析等等工作。利用LTP進行分詞，接著對詞語進行清洗，清洗過程包括單詞翻譯、分析停用詞；最后通過標準化(詞干提取和詞形還原)得到關鍵詞集合。

圖2 關鍵詞提取流程

本文采用的關鍵詞提取算法為TextRank算法[18]。

TextRank 模型表示為一個有向有權G=(V，E) 由點集合V和邊集合E組成，E是V×V的子集

WS(Vi)=(1-d)+d*∑nViwij∑VkwjkWS

(1)

式(1)表示的是TextRank中一個單詞長度i的權重取決于與在長度i前面的各個點長度j組成的長度 (j，i) 這條邊的權重，以及長度j這個點到其它邊的權重之和。

WS(Vi) 表示的是句子的權重，右側的求和表示每個相鄰句子對本句子的貢獻程度，在單文檔中本文可以大致認為所有的句子都是相鄰的，不需要像多文檔一樣進行多個窗口的生成和抽取。Wij表示兩個句子的相似度，WS表示上次迭代出句子的權重，d為阻尼系數，一般為0.85。

例如，文本中有句子“通過貸款人數據信息，并進行風險分析”，“風險”和“分析”均屬于候選關鍵詞，則組合成“風險分析”加入關鍵詞序列。最后得到DataSet{d1，d2，…，di} 集合。DataSet集合是所有數據屬性和調用操作的集合，是通過TextRank算法從需求文檔中得到的。

1.2 基于注釋UML模型的LTL生成算法

基于注釋UML模型的LTL生成算法流程如圖3所示。

圖3 基于注釋UML模型的LTL生成算法流程

LTL生成算法采用UML模型m和關鍵詞集合作為輸入，輸出一組LTL語句。首先對UML進行注釋，通過分析注釋后的UML模型得到GuardSet集合 {g1，g2，…，gi} (GuardSet集合是關于DataSet集合的一組使用條件)。接著對GuardSet集合進行遍歷得到狀態d，判斷d是否是調用操作，若是調用操作則生成一條相應的調用操作LTL語句。若不是，則判斷d是否為數據屬性，若是則生成一個相應的數據屬性LTL語句。否則將d歸類為非法數據，開始判斷下一個狀態d。

1.2.1 注釋UML模型

在處理需求文檔時，將UML模型用數據信息進行注釋，產生的文件稱為UML模型的UML注釋文件(UMLnotes)。UMLnotes內容是UML的擴展并允許相關的數據在UML模型中指定數據信息。還引入了UML安全概要UMLsec的子概要。UMLnotes 的一些信息在注釋UML模型簡介見表1。

表1 注釋UML模型簡介

在生成LTL語句過程中，在UMLnotes配置文件中有一個稱為“《critical》”的類型，這是從UMLsec配置文件中重用的一個類型。在 UMLsec中此構造型注釋可能包含數據的類。在本文的工作中，使用了這個擴展類型來注釋可能包含受需要驗證的字符類。如表1所示，擴展了這個帶有{protectedData}標簽的構造型允許定義受保護的字符與注釋為《critical》的類有關的特征。

《interpretation domain》注釋了一個模型狀態機，它會去記錄類的會發生的行為，將其注釋為一些標簽注釋UML所包含的標簽如圖4所示。本文的模型包含以下幾個標簽。

圖4 注釋UML所包含的標簽

(1){senDecisions}標簽，它允許定義特定數據屬性的設置值或調用操作事件是不應該基于特定的一些屬性。

(2){expData}標簽，它允許定義使用一些數據屬性來區分是可以接受的狀態。

(3){metric}和{threshold}標簽。這些標簽可用于根據模型的歷史數據庫識別屬性的數據以防數據信息不可用。{metric}和{threshold}標簽允許指定要使用的相關度量和數字成為驗證標準。對于靈活性問題，不限制規格{metric}標記到一組特定的指標，只要它具有到實現中的函數的映射即可，此標簽就可以將任何字符串作為輸入。

實現過程見LTL自動生成算法如算法1所示的第(1)行～第(6)行中。

1.2.2 對UML模型狀態分類

接下來對于每個被定義為數據屬性的，將執行以下操作：所有可以分配給di的可能值將從UML模型m中檢索并存儲在rangeSet中。rangeSet會將驗證模型用到的數據分配給di。

當di∈DataSet是數據屬性時如式(2)所示

LTLgidi={(gi→◇di==ti)，！(gi→◇di==ti)}

(2)

在算法的假設中，可以分配給數據屬性的可能值的數量是有限的。按照規則，屬于LTLgidi的每一對由兩個聲明組成：

(1)如果gi條件為真，數據屬性di的值最終將等于ti。

(2)如果gi條件為假，數據屬性di的值最終將等于ti。 其中，ti是可分配給si的一個可能值。

當di是調用操作事件時如式(3)所示

LTLgidi={(gi→◇eventquenue？[calld]i==ti)，！(gi→◇eventquenue？[calld]i==ti)}

(3)

在這種情況下，LTL由一對兩個聲明組成：

(1)如果gi條件為真，調用操作事件call_di最終將被添加到事件隊列中。

(2)如果gi條件為假，調用操作事件call_di最終將添加到事件隊列中。

實現過程見算法1的第(4)行～第(16)行中。

1.2.3 生成LTL語句

在算法中還聲明了一個空集LTL。該集合將用于算法來存儲可以生成的所有LTL。

對于圖3中每個使用數據的條件gi， 相對于di， 一條LTL語句將被定義如下：對于每個value屬于rangeSet，將定義一對聲明和添加到LTL中。每對聲明都應具有其對應的線性時間邏輯的格式。遍歷rangeSet中的所有值后，該LTL將被添加到LTL總的集合中。對于圖3中每個定義為調用操作的事件，將執行以下操作：對于每個使用的條件gi， 一條LTL語句將被生成。每個生成的LTL將被添加到LTL總的集合中。

實現過程見算法1的第(17)行～第(38)行中。

算法1：LTL自動生成算法

(1)generateLTL (m, Requirements);

(2)Inputs: a UML model m and a Requirements

(3)Output: a set of batches of LTL

(4)P← ?

(5)P←Participle(Requirements);

(6)sm←getIndividualFairnessStateMachine(m);

(7)DataSet←?;

(8)guardSet←?;

(9)DataSet←P.data;

(10)guardSet←getGaurds(m);

(11)LTL←?;

(12)foreach state ∈ model do

(13) expSet←?;

(14) expSet←getExplanatory(sm,state);

(15) usedConditionsSet←?;

(16) usedConditionsSet←getUsedConditions(m,P,DataSet,sm, guardSet);

(17) if state is a data attribute then

(18) rangeSet←?;

(19) rangeSet←getRange(state, m);

(20) foreach g ∈ usedConditionsSet do

(21) batch←?;

(22) foreach v ∈ rangeSet do

(23) batch.add(

(24) {g→<>state == v}, {!g→<>state==v});

(25) end

(26) LTL.add(batch);

(27) end

(28)end

(29)else

(30) foreach g∈usedConditionSet do

(31) batch←?;

(32) batch.add(

(33) {g→<>(event_queues?[call_s])},{!g→<>(event_queues?[call_s])});

(34) LTL.add(batch);

(35) end

(36) end

(37)end

(38)return LTL

2 實驗和結果

本文采用模型驗證的流程來驗證生成LTL語言的準確性。模型檢驗流程如圖5所示，展示的是模型驗證的一般流程。首先利用轉換轉換規則將UML模型轉換為Promale驗證語言。根據本文生成的LTL語句，通過使用SPIN model checker來驗證模型，以此來研判本文生成LTL語句的準確性。

圖5 模型檢驗流程

2.1 LTL自動生成案例

貸款管理系統基于真實業務流程模型，該模型由荷蘭金融機構的事件日志生成。貸款管理系統包括兩個主要流程，即貸款申請管理和風險分析管理。前者驗證是否會接受貸款請求。后者為每個接受的貸款請求創建一個貸款申請，并進行風險分析，以決定是否批準該申請。本文從StatlogCredit數據集中提取數據，該數據集存儲了1000條數據。實驗的目標是檢查如果兩個貸款申請人的數據在特定的地方存在差異，是否會調用風險分析方法。

貸款管理系統設計模型如圖6所示顯示了貸款管理系統設計的模型。實驗檢測creditHistoryStatus和save相關的部分。UML類圖，類圖通過顯示軟件的類、它們的屬性、操作以及類之間的關系來描述軟件的結構。此類圖中的一個類是“LoanManagement”。

圖6 貸款管理系統設計模型

“citizenship”是一個字符串數據屬性。代表貸款申請人的國籍?！癵ender”是一個布爾類型屬性。表明一個申請人的性別，“男”為true，“女”則為false?！癆ge>=50”是一個布爾類型屬性，表示一個貸款申請人的年齡是否大于50歲，“marital status”是一個布爾類型屬性，表示貸款申請人是否已婚，“creditHistoryStatus”是一個布爾類型屬性，如果貸款申請人有很好的信用記錄則為“true”，否則為“false”?！皊aving”是一個整數類型屬性，表示貸款申請人的存款數目。

操作的一個示例是“verifyProposal()”。在模型注釋完成后可以表示“LoanManagement”類的對象可以接收到的信號，并在模型的生命周期內接收。物體對接收到的信號作出反應并找到到其類的指定行為。

圖6是一個UML狀態機它描述“LoanManagement”類行為。UML狀態機描述實體(例如對象)的狀態序列，例如調用操作，連同它的響應動作。狀態機包含狀態和轉換。狀態表示的是執行狀態機行為的一種情況，在此期間某些不變條件成立，狀態用方框表示。

圖6中的狀態是“空閑”和“riskAnalysis”。該狀態可以是調用操作或接收到的信號，它的動作可以是一個屬性的數據分配，一個調用操作或發送信號。在圖6中，如果一個對象在“verifyProposal()”中狀態和條件 “[creditHistoryStatus==false&&saving>=1000==false]” 是true，并進入“riskAnalysis”狀態。若分析結果為“yes”則接受用戶貸款。

貸款管理系統的需求如下：

系統應提供貸款申請管理和風險分析管理的功能，前者驗證是否會接受貸款請求。后者為每個接受的貸款請求創建一個貸款申請，通過貸款人數據信息，并進行風險分析，以決定是否批準該申請。具體見貸款人數據信息說明見表2。

表2 貸款人數據信息說明

2.2 生成線性時態邏輯

在貸款管理系統示例中，通過1.2中的基于注釋UML模型的LTL生成算法，首先，以成對LTL語句的要求表達“信用狀態”對“存款”的所有組合，其中每對LTL要求單獨考慮關于一個可能屬性的聲明要求。其次驗證是否恰好一對的聲明得到滿足(即，最終為真)，而另一對的聲明被違反(即，始終為假)。也就是說，“信用狀態”與“存款”沒有關聯。這些產生的效果表示為成對的LTL聲明，即p1和p2。p1的LTL對“信用狀態”屬性檢查“調用風險分析”是否為真，p2的LTL對“存款”屬性檢查其是否為假。

(ltl claim1{(LoanRequest_creditHistoryStatus== true) -> <>(event_ queues[1]? [call riskAnalysis])},

ltl claim2{(LoanRequest_ creditHistoryStatus== true) -> <>(event. queues[1]? [call_riskAnalysis]})p1

(ltl claim3{(LoanRequest_saving>= 1000) -> <>(event_ queues[1]? [call_riskAnalysis])},

ltl claim4{!(LoanRequest_saving>=1000)-><>(event_queues[1]? [call_riskAnalysis])})p2

2.3 驗證生成線性時態邏輯的準確性

在生成一批LTL驗證語句之后，實驗根據LTL語句驗證UML模型。利用p1和p2去驗證圖6的UML模型的正確性。驗證結果見貸款管理系統驗證結果見表3。

表3 貸款管理系統驗證結果

為了解釋結果，本文用模型檢查器為違反的LTL語句生成的反例。從生成的事件跟蹤部分如算法2所示的是一個節選的痕跡Spin事件，作為違反示模型中p1，p2兩個聲明的反例。考慮圖6的兩條說明：“LoanRequest_credit-HistoryStatus = 0”，“LoanRequest_saving >=1000審批與存款和信用狀態之間存在聯系。

算法2：生成的事件跟蹤部分代碼

(1)claim claim2

(2)LoanPrposal 5 [9] 10 loanSystem.pml:14 ((!(!(!((LoanRe-quest_saving>=1000))))&&!(event_queues[1]?[4])))

(3)LoanPrposal 5 [1] 5 loanSystem.pml:14 (1)

(4)LoanPrposal 10 [10] 10 loanSystem.pml:19 (!(event_queues[1]?[4]))

(5)claim claim4

(6)LoanPrposal 5 [3] 10 loanSystem.pml:36 ((!(!(!((LoanRe-quest_creditHistoryStatus==1))))&&!(event_queues[1]?[4])))

(7)LoanPrposal 5 [1] 5 loanSystem.pml:36 (1)

(8)LoanPrposal 10 [4] 10 loanSystem.pml:41 (!(event_queues[1]?[4]))

2.4 實驗結果

實驗還利用上述方法對另外4個系統進行研究。

(1)學校獎學金管理系統，該系統描述學生申請學校獎學金的情況。在系統的活動中，結果是獎學金申請成功與否，但是需求中要求它不應根據申請人的個人特征(如性別和身體健康狀況)來影響獎學金申請成功。本文創建了一個數據集以檢查其模型與需求的一致性。該數據集包含20個人的6個數據屬性。

(2)快遞管理系統，以亞馬遜配送管理系統為基礎，展示了一個真實的事件。基于事件描述設計了交付系統的UML模型。亞馬遜的軟件為那些訂單超過35美元，并且住在亞馬遜商店附近的郵政區里的主要客戶提供免費送貨服務。本文創建了一個包含30個人5個數據屬性的數據集來驗證模型的一致性。

(3)精簡電梯模型，電梯的功能包括上行、下行、報警、顯示、開/關門等。在驗證過程中可以增加一條和某一行為需求描述相似的變遷，對其進行取反操作，觀察模型檢驗能否檢測出與需求不一致的行為。本文創建了一個包含20個人4個數據屬性的數據集來驗證模型的一致性。

(4)前主槳舵機系統，前主槳舵機是飛行控制系統的執行機構，接受來自電傳控制計算機的指令，進行相應的動作，拉動傾斜器前傾或后傾，以實現對飛機的俯仰控制。對其旋轉直接驅動閥(rotary direct drive valve，RDDV)模塊進行檢驗。本文創建了一個包含15條3個數據屬性的數據集來驗證模型的一致性。

UML模型的概述見表4。第二列顯示了模型中UML元素的數量。例如，貸款系統模型由27個要素組成。元素的數量包括類、屬性、操作、狀態機、狀態和轉換的數量。第三列和第四列分別提供了模型生成的LTL語句數量和驗證所需的時間。例如，貸款系統模型產生了4項LTL語句。Spin模型檢查器花了36 s來驗證這4項聲明，成功驗證并發現了模型中存在的錯誤。這些測試工作是在一臺配有Intel i5處理器和16 GB內存的計算機上進行的。

表4 UML模型的概述

表4提供了分析模型中檢測到的一致性違規數量。對于每個檢測到的不一致行為，該表提供了：①違規行為發生的受保護數據；②違規行為的來源(即，導致違規行為的數據段)；③違規行為是由于數據流還是直接使用違規行為源而發生的。例如，在觸發“riskAnalysis()”調用操作時，該表顯示了貸款系統模型違反了需求模型一致性，其中兩項錯誤違反由于“信用狀態”和“存款”而發生的。

2.5 實驗對比

由于現有針對軟件需求文檔UML模型等編程語言模型的形式化驗證的研究比較缺乏，歷史有關研究并不多，因此本文利用已有的ST語言模型形式化驗證方法與本文提出的基于注釋UML模型的LTL生成方法驗證模型的時間效率進行分析和對比。文獻[19]提出一種ST語言模型形式化驗證方法。首先針對ST語言模型進行分解，通過數據流分析得到模型程序依賴圖，最后根據程序依賴圖生成NuSMV的輸入模型。ST語言模型形式化驗證方法的研究對象為邏輯控制器程序，與本文的研究對象模型與需求的一致性比較類似，其中實例的模型都利用程序語言編寫。兩種方法都利用了模型形式化檢測工具，所以可以進行時間效率的對比，兩種方法的對比見ST模型與UML模型形式化驗證方法對比見表5。

實驗將貸款管理系統、獎學金管理系統、快遞管理系統、精簡電梯模型、前主槳舵機系統共5個UML模型，將本文驗證方法和ST程序模型驗證方法進行對比實驗，每種系統模型測試3次，然后計算模型驗證花費時間的平均值。本文提出的基于注釋的UML模型的LTL生成方法測試結果在UML模型驗證性能分析圖如圖7所示；ST語言模型形式化驗證方法測試結果在ST模型驗證性能分析如圖8所示。在圖7兩條折線分別代表基于注釋UML模型到驗證語句的生成時間(UML_LTL時間)以及總時間。圖8所示兩條折線分別表示ST模型到程序依賴圖生成時間(PDG時間)，以及總時間。

圖7 UML模型驗證性能分析

圖8 ST模型驗證性能分析

由圖7所示可得，UML模型到LTL語句轉換耗時較少，在UML模型代碼行數較少時，生成中間模型耗時較少，并且隨著UML模型規模的增加，總時間增長比較緩慢，說明本文提出的基于注釋UML模型的LTL生成方法更適合規模較大模型的轉換與驗證。

由圖8所示可得，由ST模型到中間狀態生成消耗時間較多，NuSMV模型驗證花費時間較少。在ST模型規模不大時，程序依賴圖生成過程花費的時間相對較多，隨著ST模型規模的增加，總時間增長緩慢。說明針對模型規模較小的ST模型在生成中間狀態過程中效率相對較低，不適合規模較大的模型進行轉換。

由對比結果可以了解到，本文的基于注釋UML模型的LTL生成方法的時間效率優于已有的ST語言模型轉換方法生成NuSMV模型的時間效率，并且適合各種規模模型的驗證。

3 結束語

基于注釋UML模型的LTL驗證語句自動生成方法，經過了一個完整的模型驗證過程，發現可以提高了模型檢測的效率并能準確發現模型中存在的錯誤，減少了測試人員模型檢測的時間。目前存在的問題是：本文的方法搜索單個屬性LTL驗證語句，而有時一個LTL驗證語句需要用到多個屬性。由于UML模型具有很大的可變性，因此無法保證生成完整的LTL語句。為了解決這些問題需要考慮多屬性LTL語句，確定開發人員在建模過程中必須遵循的約束，以便驗證生成的LTL驗證語句的完整性。優化自然語言處理算法對需求文檔關鍵詞的提取過程，用以豐富生成的LTL驗證語句中的屬性。