徐光會，高俊濤

(東北石油大學(xué),計算機(jī)與信息技術(shù)學(xué)院，黑龍江,大慶 163318)

0 引言

軟件模型在軟件系統(tǒng)的整個生命周期中起著重要的作用。通過模型，軟件工程師可以獲得對系統(tǒng)行為的深刻理解，而無需處理復(fù)雜的實(shí)現(xiàn)。盡管良好的軟件工程實(shí)踐建議應(yīng)該在獲得實(shí)現(xiàn)之前預(yù)先開發(fā)模型，但現(xiàn)實(shí)顯示，模型經(jīng)常不存在，或者它們與實(shí)現(xiàn)不一致。事實(shí)上，建立一個合適的模型是昂貴的，困難的，并且需要數(shù)學(xué)技能和獨(dú)創(chuàng)性。此外，即使開發(fā)了模型，它們通常也不會隨著實(shí)現(xiàn)中的更改而更新，因此模型和實(shí)現(xiàn)逐漸發(fā)生分歧。

模型推理是解決這一問題的一種很有前途的方法，它使用機(jī)器學(xué)習(xí)從執(zhí)行日志中自動推斷軟件行為模型。精確捕獲軟件系統(tǒng)的模型對于廣泛的軟件維護(hù)和驗證是有用的。最近的研究提出了許多被動學(xué)習(xí)模型推理技術(shù)，大多數(shù)推理技術(shù)都是將軟件系統(tǒng)的一組執(zhí)行軌跡作為輸入，并推斷出模型，比如Synoptic[1]、InvariMint[2]、flexfringe[3]、CSight[4]、MINT[5]、GK-tail+[6]和2017年Rick Wieman等[7]推斷大型支付系統(tǒng)的模型等。

本文主要從以下幾個方面對軟件模型推斷領(lǐng)域的研究成果進(jìn)行綜述：①軟件模型推斷的相關(guān)定義；②軟件模型推斷過程；③軟件模型被動學(xué)習(xí)推斷技術(shù)；④總結(jié)與展望。

1 相關(guān)定義

1.1 軌跡和事件不變量

定義 1 (事件和軌跡)事件是一個元組(l,v)，其中l(wèi)是一個函數(shù)的名稱，v是l的參數(shù)變量到具體值的映射。軌跡t∈T是一個有限的事件序列，通常寫為〈(l0,v0),…(ln,vn)〉。

定義 2 (正軌跡和負(fù)軌跡)對于給定系統(tǒng)，正軌跡代表了可能出現(xiàn)的系統(tǒng)可行的行為，負(fù)軌跡代表了不可能出現(xiàn)的行為。

定義 3 (日志)日志是由一組軌跡組成。

定義 4 (事件不變量)：假設(shè)a和b是2種事件，3種事件不變量如下。

(1)a總是跟在b后面(aAlways Followed Byb，寫為a→b)。每當(dāng)事件a出現(xiàn)時，事件b總是出現(xiàn)在同一軌跡的后面。

(2)a從不跟b(aNever Followed Byb，寫為a→/b)。每當(dāng)出現(xiàn)事件a時，事件b就永遠(yuǎn)不會再出現(xiàn)在同一軌跡中。

(3)a始終位于b前面(aAlways Precedesb，寫為a←b)。每當(dāng)出現(xiàn)事件b時，事件a總是出現(xiàn)在同一軌跡中的b之前。

1.2 狀態(tài)機(jī)

定義 5 (有限狀態(tài)機(jī)-Finite State Machine，F(xiàn)SM)的定義是一個六元組

F=(Q,X,Y,q0,δ,O)

(1)

其中,Q表示有窮的狀態(tài)集合,X表示有窮的輸入集合,Y表示有窮的輸出集合,q0∈Q，是FSM模型的初始狀態(tài),δ:Q×X→Q，是狀態(tài)轉(zhuǎn)換函數(shù),O:Q×X→O，是輸出函數(shù)。通常，有限狀態(tài)機(jī)指的是確定性有限自動機(jī)(DFA)或非確定性有限自動機(jī)(NFA)。

2 軟件模型推斷過程

軟件模型推斷過程從“信息收集”的過程開始，可能涉及到對源代碼的分析、對程序執(zhí)行的觀察，或者兩者的某種結(jié)合。這些信息通常被抽象出來，即它必須在有用的細(xì)節(jié)級別上捕獲程序中相關(guān)的興趣點(diǎn)，以便最終的結(jié)果是可讀的和相關(guān)的。最后，所收集的信息用于推斷軟件行為模型。

對程序執(zhí)行觀察的軟件模型推斷過程一般所涉及的關(guān)鍵步驟如圖1所示。所有軟件模型推斷的過程都可以用這些步驟來描述，從目標(biāo)軟件系統(tǒng)執(zhí)行行為中獲取關(guān)鍵信息，形成推斷模型所需要的軌跡，然后用推斷軟件模型的技術(shù)推斷目標(biāo)軟件模型，最后將生成的模型反饋給開發(fā)維護(hù)人員幫助理解系統(tǒng)和開發(fā)維護(hù)系統(tǒng)。

圖1 軟件推斷模型過程

3 軟件模型被動學(xué)習(xí)推斷技術(shù)

3.1 Synoptic

Synoptic是由BESCHASTNIKH等[1]在2011年提出的，Synoptic總是能生成一個精確滿足從日志中挖掘出的事件不變量的模型，開發(fā)人員使用Synoptic生成的模型來驗證已知的bug，診斷新的bug，并增加他們對系統(tǒng)正確性的信心和改進(jìn)開發(fā)人員對系統(tǒng)的理解。

Synoptic核心算法是BisimH，BisimH算法首先根據(jù)正則表達(dá)式從日志中提取的信息構(gòu)建軌跡圖，從軌跡圖挖掘3種事件不變量，將具有相同軌跡標(biāo)識符劃分一起，并分別構(gòu)建軌跡圖(步驟1)。根據(jù)軌跡圖，構(gòu)建初始模型，初始模型是最緊湊或最抽象的模型(步驟2)。然后進(jìn)行細(xì)化和粗化，這是Synoptic的雙重操作。從初始模型開始，首先對模型進(jìn)行細(xì)化，判斷初始模型是否違反事件不變量，BisimH使用一個基于FSM的模型檢查器來檢查模型是否滿足挖掘的不變量。如果違反事件不變量，則將違反事件不變量的軌跡作為反例來細(xì)化模型，直到生成的模型滿足所有的事件不變量(步驟3)。當(dāng)細(xì)化完成后，進(jìn)行粗化，當(dāng)無法進(jìn)一步粗化模型時，生成最終的模型(步驟4)。

Synoptic根據(jù)購物車應(yīng)用程序的日志構(gòu)建的模型如圖2所示，該購物車程序包含事件check-out,valid-coupon,reduce-price,get-credit-card。

Synoptic根據(jù)圖2頂部的日志和正則表達(dá)式，將日志解析為3個軌跡，每個軌跡對應(yīng)訪問服務(wù)器的3個用戶IP地址，分別是74.15.155.103、74.15.232.201、13.15.232.201。根據(jù)這3個IP地址分別構(gòu)建軌跡圖，根據(jù)軌跡圖構(gòu)建初始模型，經(jīng)過細(xì)化和粗化過程生成最終的軟件模型。

圖2 Synoptic根據(jù)購物車應(yīng)用程序的日志構(gòu)建的模型

3.2 InvariMint

InvariMint是由BESCHASTNIKH等[2]在2013年提出的，是一種以聲明方式指定模型推理算法的方法。InvariMint擴(kuò)展和比較了現(xiàn)有的算法，方便比較和對比先前發(fā)表的算法，并且使用InvariMint指定的算法比原本的算法表現(xiàn)得更好。

InvariMint是一種描述模型推理算法的方法，或者說是一種公共語言。InvariMint的目標(biāo)本身并不是生成模型，而是提供一種用于表示或指定模型推理算法的公共語言，使用相同的語言執(zhí)行不同的算法可以讓我們理解、組合和比較這些算法。

InvariMint將一個軌跡日志作為輸入，并輸出一個推斷模型，該模型描述輸入日志的過程。在內(nèi)部，該算法使用日志屬性類型來挖掘?qū)傩詫?shí)例，然后將組合函數(shù)應(yīng)用于屬性實(shí)例來派生模型。

一個簡單的郵件客戶端例子如圖3所示，包含事件login,check,compose,send,logout。InvariMint可根據(jù)輸入的兩條軌跡生成描述輸入日志的模型。

圖3 InvariMint生成郵件客戶端系統(tǒng)的模型

3.3 flexfringe

flexfringe[3]工具可以從軌跡中推斷軟件系統(tǒng)的模型，是一種開源代碼軟件工具，可使用最先進(jìn)的證據(jù)驅(qū)動狀態(tài)合并算法從軌跡中學(xué)習(xí)有限狀態(tài)自動機(jī)的變體。通過提供靈活、可擴(kuò)展的界面，滿足了在不同應(yīng)用程序域中對定制模型和定制學(xué)習(xí)啟發(fā)式的需求。

flexfringe核心算法是證據(jù)驅(qū)動的狀態(tài)合并算法和概率變量，以使用一致性檢查和得分功能的啟發(fā)式搜索為中心，可以處理各種啟發(fā)式和模型類型。flexfringe工具有效實(shí)現(xiàn)了狀態(tài)合并算法、尋找更好模型的搜索方法、狀態(tài)合并算法的高級功能、修改flexfringe核心功能和搜索策略的許多參數(shù)、通過向代碼中添加單個文件來修改模型的啟發(fā)式和類型及其可視化的能力和提供交互式界面，允許用戶修改算法的不同步驟，以微調(diào)新定義的啟發(fā)式算法。

flexfringe工具的目標(biāo)是為從業(yè)人員提供不僅方便且易于使用的工具，而且?guī)椭麄冊跓o需深入了解核心狀態(tài)合并算法的情況下構(gòu)建自定義的模型。

使用flexfringe工具生成支付系統(tǒng)的模型如圖4所示。將支付系統(tǒng)的相關(guān)執(zhí)行日志作為輸入，flexfringe可生成對應(yīng)的軟件模型。

圖4 flexfringe生成支付系統(tǒng)模型

4 總結(jié)

本文對目前的軟件模型推斷過程和被動學(xué)習(xí)技術(shù)推斷模型進(jìn)行了概述，雖然目前已經(jīng)實(shí)現(xiàn)了很多軟件模型推斷技術(shù)，比如Synoptic、InvariMint和flexfringe等，但這些軟件模型推斷技術(shù)依舊存在一些問題還需要解決。

正負(fù)軌跡問題。目前大部分軟件模型推斷技術(shù)只考慮了正軌跡，并沒有考慮負(fù)軌跡，但在軟件系統(tǒng)運(yùn)行的實(shí)際情況中，并不僅僅有正常執(zhí)行的軌跡，還存在一些異?；虿荒苷?zhí)行的軌跡。因此，未來可以開發(fā)以正負(fù)樣本算法為核心的工具，用來構(gòu)建正負(fù)軌跡的模型。

軟件模型評估問題。目前軟件模型推斷技術(shù)可以生成軟件系統(tǒng)的模型，但目前論文中并沒有評估模型的標(biāo)準(zhǔn)。因此，未來可以提出一些評估模型的標(biāo)準(zhǔn)。