面向模型檢測(cè)的LTL語(yǔ)句自動(dòng)生成方法

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

(1.南昌航空大學(xué) 軟件學(xué)院，江西 南昌 330063；2.南昌航空大學(xué) 軟件測(cè)評(píng)中心，江西 南昌 330063)

0 引 言

模型檢測(cè)作為軟件系統(tǒng)驗(yàn)證中的一個(gè)常用手段，已經(jīng)在多個(gè)領(lǐng)域得到了應(yīng)用。在基于模型開(kāi)發(fā)的軟件系統(tǒng)驗(yàn)證中，線性時(shí)態(tài)邏輯LTL(linear-time temporal logic)用于描述軟件的性質(zhì)，這些性質(zhì)又被稱為線性時(shí)間屬性。這是邁向構(gòu)建模型檢測(cè)理論重要的一步，現(xiàn)已得到了廣泛的應(yīng)用[1-4]。

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

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

本文提出了一個(gè)基于自然語(yǔ)言處理的線性時(shí)態(tài)邏輯自動(dòng)生成的方法，支持基于模型的開(kāi)發(fā)軟件設(shè)計(jì)的分析。在本文的方法中，通過(guò)自動(dòng)生成線性時(shí)態(tài)邏輯聲明來(lái)建立來(lái)對(duì)模型與需求的進(jìn)行一致性分析。本文研究的目標(biāo)是減少在軟件開(kāi)發(fā)后期檢測(cè)需求模型一致性所需的工作。

1 本文工作

本文提出的LTL語(yǔ)句自動(dòng)生成方法如圖1所示。本文采用的輸入是需求說(shuō)明書(shū)和UML模型，然后采用關(guān)鍵詞提取，基于注釋UML模型的LTL生成方法，從而生成LTL語(yǔ)句。

圖1 LTL語(yǔ)句自動(dòng)生成方法

1.1 關(guān)鍵詞提取

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

圖2 關(guān)鍵詞提取流程

本文采用的關(guān)鍵詞提取算法為T(mén)extRank算法[18]。

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

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

(1)

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

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

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

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

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

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

LTL生成算法采用UML模型m和關(guān)鍵詞集合作為輸入，輸出一組LTL語(yǔ)句。首先對(duì)UML進(jìn)行注釋，通過(guò)分析注釋后的UML模型得到GuardSet集合 {g1，g2，…，gi} (GuardSet集合是關(guān)于DataSet集合的一組使用條件)。接著對(duì)GuardSet集合進(jìn)行遍歷得到狀態(tài)d，判斷d是否是調(diào)用操作，若是調(diào)用操作則生成一條相應(yīng)的調(diào)用操作LTL語(yǔ)句。若不是，則判斷d是否為數(shù)據(jù)屬性，若是則生成一個(gè)相應(yīng)的數(shù)據(jù)屬性LTL語(yǔ)句。否則將d歸類(lèi)為非法數(shù)據(jù)，開(kāi)始判斷下一個(gè)狀態(tài)d。

1.2.1 注釋UML模型

在處理需求文檔時(shí)，將UML模型用數(shù)據(jù)信息進(jìn)行注釋，產(chǎn)生的文件稱為UML模型的UML注釋文件(UMLnotes)。UMLnotes內(nèi)容是UML的擴(kuò)展并允許相關(guān)的數(shù)據(jù)在UML模型中指定數(shù)據(jù)信息。還引入了UML安全概要UMLsec的子概要。UMLnotes 的一些信息在注釋UML模型簡(jiǎn)介見(jiàn)表1。

表1 注釋UML模型簡(jiǎn)介

在生成LTL語(yǔ)句過(guò)程中，在UMLnotes配置文件中有一個(gè)稱為“《critical》”的類(lèi)型，這是從UMLsec配置文件中重用的一個(gè)類(lèi)型。在 UMLsec中此構(gòu)造型注釋可能包含數(shù)據(jù)的類(lèi)。在本文的工作中，使用了這個(gè)擴(kuò)展類(lèi)型來(lái)注釋可能包含受需要驗(yàn)證的字符類(lèi)。如表1所示，擴(kuò)展了這個(gè)帶有{protectedData}標(biāo)簽的構(gòu)造型允許定義受保護(hù)的字符與注釋為《critical》的類(lèi)有關(guān)的特征。

《interpretation domain》注釋了一個(gè)模型狀態(tài)機(jī)，它會(huì)去記錄類(lèi)的會(huì)發(fā)生的行為，將其注釋為一些標(biāo)簽注釋UML所包含的標(biāo)簽如圖4所示。本文的模型包含以下幾個(gè)標(biāo)簽。

圖4 注釋UML所包含的標(biāo)簽

(1){senDecisions}標(biāo)簽，它允許定義特定數(shù)據(jù)屬性的設(shè)置值或調(diào)用操作事件是不應(yīng)該基于特定的一些屬性。

(2){expData}標(biāo)簽，它允許定義使用一些數(shù)據(jù)屬性來(lái)區(qū)分是可以接受的狀態(tài)。

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

實(shí)現(xiàn)過(guò)程見(jiàn)LTL自動(dòng)生成算法如算法1所示的第(1)行～第(6)行中。

1.2.2 對(duì)UML模型狀態(tài)分類(lèi)

接下來(lái)對(duì)于每個(gè)被定義為數(shù)據(jù)屬性的，將執(zhí)行以下操作：所有可以分配給di的可能值將從UML模型m中檢索并存儲(chǔ)在rangeSet中。rangeSet會(huì)將驗(yàn)證模型用到的數(shù)據(jù)分配給di。

當(dāng)di∈DataSet是數(shù)據(jù)屬性時(shí)如式(2)所示

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

(2)

在算法的假設(shè)中，可以分配給數(shù)據(jù)屬性的可能值的數(shù)量是有限的。按照規(guī)則，屬于LTLgidi的每一對(duì)由兩個(gè)聲明組成：

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

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

當(dāng)di是調(diào)用操作事件時(shí)如式(3)所示

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

(3)

在這種情況下，LTL由一對(duì)兩個(gè)聲明組成：

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

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

實(shí)現(xiàn)過(guò)程見(jiàn)算法1的第(4)行～第(16)行中。

1.2.3 生成LTL語(yǔ)句

在算法中還聲明了一個(gè)空集LTL。該集合將用于算法來(lái)存儲(chǔ)可以生成的所有LTL。

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

實(shí)現(xiàn)過(guò)程見(jiàn)算法1的第(17)行～第(38)行中。

算法1：LTL自動(dòng)生成算法

(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 實(shí)驗(yàn)和結(jié)果

本文采用模型驗(yàn)證的流程來(lái)驗(yàn)證生成LTL語(yǔ)言的準(zhǔn)確性。模型檢驗(yàn)流程如圖5所示，展示的是模型驗(yàn)證的一般流程。首先利用轉(zhuǎn)換轉(zhuǎn)換規(guī)則將UML模型轉(zhuǎn)換為Promale驗(yàn)證語(yǔ)言。根據(jù)本文生成的LTL語(yǔ)句，通過(guò)使用SPIN model checker來(lái)驗(yàn)證模型，以此來(lái)研判本文生成LTL語(yǔ)句的準(zhǔn)確性。

圖5 模型檢驗(yàn)流程

2.1 LTL自動(dòng)生成案例

貸款管理系統(tǒng)基于真實(shí)業(yè)務(wù)流程模型，該模型由荷蘭金融機(jī)構(gòu)的事件日志生成。貸款管理系統(tǒng)包括兩個(gè)主要流程，即貸款申請(qǐng)管理和風(fēng)險(xiǎn)分析管理。前者驗(yàn)證是否會(huì)接受貸款請(qǐng)求。后者為每個(gè)接受的貸款請(qǐng)求創(chuàng)建一個(gè)貸款申請(qǐng)，并進(jìn)行風(fēng)險(xiǎn)分析，以決定是否批準(zhǔn)該申請(qǐng)。本文從StatlogCredit數(shù)據(jù)集中提取數(shù)據(jù)，該數(shù)據(jù)集存儲(chǔ)了1000條數(shù)據(jù)。實(shí)驗(yàn)的目標(biāo)是檢查如果兩個(gè)貸款申請(qǐng)人的數(shù)據(jù)在特定的地方存在差異，是否會(huì)調(diào)用風(fēng)險(xiǎn)分析方法。

貸款管理系統(tǒng)設(shè)計(jì)模型如圖6所示顯示了貸款管理系統(tǒng)設(shè)計(jì)的模型。實(shí)驗(yàn)檢測(cè)creditHistoryStatus和save相關(guān)的部分。UML類(lèi)圖，類(lèi)圖通過(guò)顯示軟件的類(lèi)、它們的屬性、操作以及類(lèi)之間的關(guān)系來(lái)描述軟件的結(jié)構(gòu)。此類(lèi)圖中的一個(gè)類(lèi)是“LoanManagement”。

圖6 貸款管理系統(tǒng)設(shè)計(jì)模型

“citizenship”是一個(gè)字符串?dāng)?shù)據(jù)屬性。代表貸款申請(qǐng)人的國(guó)籍?！癵ender”是一個(gè)布爾類(lèi)型屬性。表明一個(gè)申請(qǐng)人的性別，“男”為true，“女”則為false?！癆ge>=50”是一個(gè)布爾類(lèi)型屬性，表示一個(gè)貸款申請(qǐng)人的年齡是否大于50歲，“marital status”是一個(gè)布爾類(lèi)型屬性，表示貸款申請(qǐng)人是否已婚，“creditHistoryStatus”是一個(gè)布爾類(lèi)型屬性，如果貸款申請(qǐng)人有很好的信用記錄則為“true”，否則為“false”。“saving”是一個(gè)整數(shù)類(lèi)型屬性，表示貸款申請(qǐng)人的存款數(shù)目。

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

圖6是一個(gè)UML狀態(tài)機(jī)它描述“LoanManagement”類(lèi)行為。UML狀態(tài)機(jī)描述實(shí)體(例如對(duì)象)的狀態(tài)序列，例如調(diào)用操作，連同它的響應(yīng)動(dòng)作。狀態(tài)機(jī)包含狀態(tài)和轉(zhuǎn)換。狀態(tài)表示的是執(zhí)行狀態(tài)機(jī)行為的一種情況，在此期間某些不變條件成立，狀態(tài)用方框表示。

圖6中的狀態(tài)是“空閑”和“riskAnalysis”。該狀態(tài)可以是調(diào)用操作或接收到的信號(hào)，它的動(dòng)作可以是一個(gè)屬性的數(shù)據(jù)分配，一個(gè)調(diào)用操作或發(fā)送信號(hào)。在圖6中，如果一個(gè)對(duì)象在“verifyProposal()”中狀態(tài)和條件 “[creditHistoryStatus==false&&saving>=1000==false]” 是true，并進(jìn)入“riskAnalysis”狀態(tài)。若分析結(jié)果為“yes”則接受用戶貸款。

貸款管理系統(tǒng)的需求如下：

系統(tǒng)應(yīng)提供貸款申請(qǐng)管理和風(fēng)險(xiǎn)分析管理的功能，前者驗(yàn)證是否會(huì)接受貸款請(qǐng)求。后者為每個(gè)接受的貸款請(qǐng)求創(chuàng)建一個(gè)貸款申請(qǐng)，通過(guò)貸款人數(shù)據(jù)信息，并進(jìn)行風(fēng)險(xiǎn)分析，以決定是否批準(zhǔn)該申請(qǐng)。具體見(jiàn)貸款人數(shù)據(jù)信息說(shuō)明見(jiàn)表2。

表2 貸款人數(shù)據(jù)信息說(shuō)明

2.2 生成線性時(shí)態(tài)邏輯

在貸款管理系統(tǒng)示例中，通過(guò)1.2中的基于注釋UML模型的LTL生成算法，首先，以成對(duì)LTL語(yǔ)句的要求表達(dá)“信用狀態(tài)”對(duì)“存款”的所有組合，其中每對(duì)LTL要求單獨(dú)考慮關(guān)于一個(gè)可能屬性的聲明要求。其次驗(yàn)證是否恰好一對(duì)的聲明得到滿足(即，最終為真)，而另一對(duì)的聲明被違反(即，始終為假)。也就是說(shuō)，“信用狀態(tài)”與“存款”沒(méi)有關(guān)聯(lián)。這些產(chǎn)生的效果表示為成對(duì)的LTL聲明，即p1和p2。p1的LTL對(duì)“信用狀態(tài)”屬性檢查“調(diào)用風(fēng)險(xiǎn)分析”是否為真，p2的LTL對(duì)“存款”屬性檢查其是否為假。

(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 驗(yàn)證生成線性時(shí)態(tài)邏輯的準(zhǔn)確性

在生成一批LTL驗(yàn)證語(yǔ)句之后，實(shí)驗(yàn)根據(jù)LTL語(yǔ)句驗(yàn)證UML模型。利用p1和p2去驗(yàn)證圖6的UML模型的正確性。驗(yàn)證結(jié)果見(jiàn)貸款管理系統(tǒng)驗(yàn)證結(jié)果見(jiàn)表3。

表3 貸款管理系統(tǒng)驗(yàn)證結(jié)果

為了解釋結(jié)果，本文用模型檢查器為違反的LTL語(yǔ)句生成的反例。從生成的事件跟蹤部分如算法2所示的是一個(gè)節(jié)選的痕跡Spin事件，作為違反示模型中p1，p2兩個(gè)聲明的反例?？紤]圖6的兩條說(shuō)明：“LoanRequest_credit-HistoryStatus = 0”，“LoanRequest_saving >=1000審批與存款和信用狀態(tài)之間存在聯(lián)系。

算法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 實(shí)驗(yàn)結(jié)果

實(shí)驗(yàn)還利用上述方法對(duì)另外4個(gè)系統(tǒng)進(jìn)行研究。

(1)學(xué)校獎(jiǎng)學(xué)金管理系統(tǒng)，該系統(tǒng)描述學(xué)生申請(qǐng)學(xué)校獎(jiǎng)學(xué)金的情況。在系統(tǒng)的活動(dòng)中，結(jié)果是獎(jiǎng)學(xué)金申請(qǐng)成功與否，但是需求中要求它不應(yīng)根據(jù)申請(qǐng)人的個(gè)人特征(如性別和身體健康狀況)來(lái)影響?yīng)剬W(xué)金申請(qǐng)成功。本文創(chuàng)建了一個(gè)數(shù)據(jù)集以檢查其模型與需求的一致性。該數(shù)據(jù)集包含20個(gè)人的6個(gè)數(shù)據(jù)屬性。

(2)快遞管理系統(tǒng)，以亞馬遜配送管理系統(tǒng)為基礎(chǔ)，展示了一個(gè)真實(shí)的事件。基于事件描述設(shè)計(jì)了交付系統(tǒng)的UML模型。亞馬遜的軟件為那些訂單超過(guò)35美元，并且住在亞馬遜商店附近的郵政區(qū)里的主要客戶提供免費(fèi)送貨服務(wù)。本文創(chuàng)建了一個(gè)包含30個(gè)人5個(gè)數(shù)據(jù)屬性的數(shù)據(jù)集來(lái)驗(yàn)證模型的一致性。

(3)精簡(jiǎn)電梯模型，電梯的功能包括上行、下行、報(bào)警、顯示、開(kāi)/關(guān)門(mén)等。在驗(yàn)證過(guò)程中可以增加一條和某一行為需求描述相似的變遷，對(duì)其進(jìn)行取反操作，觀察模型檢驗(yàn)?zāi)芊駲z測(cè)出與需求不一致的行為。本文創(chuàng)建了一個(gè)包含20個(gè)人4個(gè)數(shù)據(jù)屬性的數(shù)據(jù)集來(lái)驗(yàn)證模型的一致性。

(4)前主槳舵機(jī)系統(tǒng)，前主槳舵機(jī)是飛行控制系統(tǒng)的執(zhí)行機(jī)構(gòu)，接受來(lái)自電傳控制計(jì)算機(jī)的指令，進(jìn)行相應(yīng)的動(dòng)作，拉動(dòng)傾斜器前傾或后傾，以實(shí)現(xiàn)對(duì)飛機(jī)的俯仰控制。對(duì)其旋轉(zhuǎn)直接驅(qū)動(dòng)閥(rotary direct drive valve，RDDV)模塊進(jìn)行檢驗(yàn)。本文創(chuàng)建了一個(gè)包含15條3個(gè)數(shù)據(jù)屬性的數(shù)據(jù)集來(lái)驗(yàn)證模型的一致性。

UML模型的概述見(jiàn)表4。第二列顯示了模型中UML元素的數(shù)量。例如，貸款系統(tǒng)模型由27個(gè)要素組成。元素的數(shù)量包括類(lèi)、屬性、操作、狀態(tài)機(jī)、狀態(tài)和轉(zhuǎn)換的數(shù)量。第三列和第四列分別提供了模型生成的LTL語(yǔ)句數(shù)量和驗(yàn)證所需的時(shí)間。例如，貸款系統(tǒng)模型產(chǎn)生了4項(xiàng)LTL語(yǔ)句。Spin模型檢查器花了36 s來(lái)驗(yàn)證這4項(xiàng)聲明，成功驗(yàn)證并發(fā)現(xiàn)了模型中存在的錯(cuò)誤。這些測(cè)試工作是在一臺(tái)配有Intel i5處理器和16 GB內(nèi)存的計(jì)算機(jī)上進(jìn)行的。

表4 UML模型的概述

表4提供了分析模型中檢測(cè)到的一致性違規(guī)數(shù)量。對(duì)于每個(gè)檢測(cè)到的不一致行為，該表提供了：①違規(guī)行為發(fā)生的受保護(hù)數(shù)據(jù)；②違規(guī)行為的來(lái)源(即，導(dǎo)致違規(guī)行為的數(shù)據(jù)段)；③違規(guī)行為是由于數(shù)據(jù)流還是直接使用違規(guī)行為源而發(fā)生的。例如，在觸發(fā)“riskAnalysis()”調(diào)用操作時(shí)，該表顯示了貸款系統(tǒng)模型違反了需求模型一致性，其中兩項(xiàng)錯(cuò)誤違反由于“信用狀態(tài)”和“存款”而發(fā)生的。

2.5 實(shí)驗(yàn)對(duì)比

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

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

圖7 UML模型驗(yàn)證性能分析

圖8 ST模型驗(yàn)證性能分析

由圖7所示可得，UML模型到LTL語(yǔ)句轉(zhuǎn)換耗時(shí)較少，在UML模型代碼行數(shù)較少時(shí)，生成中間模型耗時(shí)較少，并且隨著UML模型規(guī)模的增加，總時(shí)間增長(zhǎng)比較緩慢，說(shuō)明本文提出的基于注釋UML模型的LTL生成方法更適合規(guī)模較大模型的轉(zhuǎn)換與驗(yàn)證。

由圖8所示可得，由ST模型到中間狀態(tài)生成消耗時(shí)間較多，NuSMV模型驗(yàn)證花費(fèi)時(shí)間較少。在ST模型規(guī)模不大時(shí)，程序依賴圖生成過(guò)程花費(fèi)的時(shí)間相對(duì)較多，隨著ST模型規(guī)模的增加，總時(shí)間增長(zhǎng)緩慢。說(shuō)明針對(duì)模型規(guī)模較小的ST模型在生成中間狀態(tài)過(guò)程中效率相對(duì)較低，不適合規(guī)模較大的模型進(jìn)行轉(zhuǎn)換。

由對(duì)比結(jié)果可以了解到，本文的基于注釋UML模型的LTL生成方法的時(shí)間效率優(yōu)于已有的ST語(yǔ)言模型轉(zhuǎn)換方法生成NuSMV模型的時(shí)間效率，并且適合各種規(guī)模模型的驗(yàn)證。

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

基于注釋UML模型的LTL驗(yàn)證語(yǔ)句自動(dòng)生成方法，經(jīng)過(guò)了一個(gè)完整的模型驗(yàn)證過(guò)程，發(fā)現(xiàn)可以提高了模型檢測(cè)的效率并能準(zhǔn)確發(fā)現(xiàn)模型中存在的錯(cuò)誤，減少了測(cè)試人員模型檢測(cè)的時(shí)間。目前存在的問(wèn)題是：本文的方法搜索單個(gè)屬性LTL驗(yàn)證語(yǔ)句，而有時(shí)一個(gè)LTL驗(yàn)證語(yǔ)句需要用到多個(gè)屬性。由于UML模型具有很大的可變性，因此無(wú)法保證生成完整的LTL語(yǔ)句。為了解決這些問(wèn)題需要考慮多屬性LTL語(yǔ)句，確定開(kāi)發(fā)人員在建模過(guò)程中必須遵循的約束，以便驗(yàn)證生成的LTL驗(yàn)證語(yǔ)句的完整性。優(yōu)化自然語(yǔ)言處理算法對(duì)需求文檔關(guān)鍵詞的提取過(guò)程，用以豐富生成的LTL驗(yàn)證語(yǔ)句中的屬性。