葉玲玲， 錢俊彥， 查顯偉

(桂林電子科技大學(xué) 計(jì)算機(jī)與信息安全學(xué)院，廣西 桂林 541004)

隨著軟件系統(tǒng)規(guī)模和復(fù)雜性的不斷增加，驗(yàn)證軟件系統(tǒng)正確性和安全性的難度也越來(lái)越大。對(duì)于大規(guī)模的軟件系統(tǒng)，傳統(tǒng)的驗(yàn)證技術(shù)(如模型驗(yàn)證[1]和測(cè)試[2])會(huì)出現(xiàn)狀態(tài)爆炸和難以覆蓋系統(tǒng)所有執(zhí)行分支等問(wèn)題。運(yùn)行時(shí)驗(yàn)證[3-4]是一種輕量級(jí)的形式化驗(yàn)證方法，它根據(jù)軟件系統(tǒng)的實(shí)際執(zhí)行情況來(lái)驗(yàn)證系統(tǒng)的正確性，能夠?yàn)槿藗兲峁┫到y(tǒng)運(yùn)行時(shí)行為的準(zhǔn)確信息。運(yùn)行時(shí)驗(yàn)證技術(shù)通過(guò)分析系統(tǒng)的一個(gè)或多個(gè)執(zhí)行軌跡來(lái)驗(yàn)證系統(tǒng)，避免了傳統(tǒng)形式化驗(yàn)證技術(shù)復(fù)雜性高的問(wèn)題。運(yùn)行時(shí)驗(yàn)證的核心部分是監(jiān)控器[3]，對(duì)系統(tǒng)進(jìn)行運(yùn)行時(shí)驗(yàn)證就是將待驗(yàn)證的系統(tǒng)置于監(jiān)控下，監(jiān)控器通過(guò)驗(yàn)證系統(tǒng)的執(zhí)行軌跡是否滿足給定的屬性來(lái)判斷系統(tǒng)是否正確。

近年來(lái)，為了確保軟件系統(tǒng)的正確性，運(yùn)行時(shí)驗(yàn)證得到了廣泛的應(yīng)用。Asadollah等[5]在多核并行軟件環(huán)境下，提出了一種基于運(yùn)行時(shí)驗(yàn)證的漏洞檢測(cè)模型，用于檢測(cè)系統(tǒng)故障；Incki等[6]運(yùn)用運(yùn)行時(shí)驗(yàn)證技術(shù)來(lái)防止物聯(lián)網(wǎng)中的網(wǎng)絡(luò)攻擊。然而，對(duì)系統(tǒng)進(jìn)行運(yùn)行時(shí)驗(yàn)證，通常會(huì)產(chǎn)生一些額外的驗(yàn)證開(kāi)銷，因此，減少運(yùn)行時(shí)驗(yàn)證工具的監(jiān)控開(kāi)銷成為了一個(gè)非常重要的研究?jī)?nèi)容。

為了減少運(yùn)行時(shí)驗(yàn)證的開(kāi)銷，Reger等[7]提出MARQ驗(yàn)證工具，通過(guò)索引技術(shù)和對(duì)監(jiān)控對(duì)象的冗余刪除來(lái)減少運(yùn)行時(shí)開(kāi)銷；Reger[8]運(yùn)用靜態(tài)分析去除運(yùn)行時(shí)驗(yàn)證不可達(dá)對(duì)象，減少需檢測(cè)的對(duì)象，從而減少監(jiān)控開(kāi)銷；Chen等[9]提出了弱監(jiān)控性的定義，排除不可監(jiān)控的屬性，以減少運(yùn)行時(shí)監(jiān)控開(kāi)銷。這些控制運(yùn)行時(shí)驗(yàn)證開(kāi)銷的方法，主要考慮的是找到并刪除無(wú)用的監(jiān)控對(duì)象。為了達(dá)到減少運(yùn)行時(shí)監(jiān)控開(kāi)銷的目的，還可以對(duì)JavaMOP[10]、TraceMatches[11]等運(yùn)行時(shí)驗(yàn)證工具生成監(jiān)控器代碼的過(guò)程進(jìn)行優(yōu)化，進(jìn)而控制監(jiān)控器在構(gòu)造過(guò)程中的開(kāi)銷。鑒于此，提出一種基于Büchi自動(dòng)機(jī)化簡(jiǎn)的監(jiān)控器構(gòu)造方法,降低JavaMOP運(yùn)行時(shí)驗(yàn)證的時(shí)間和內(nèi)存開(kāi)銷。

1 相關(guān)知識(shí)

1.1 線性時(shí)態(tài)邏輯

線性時(shí)態(tài)邏輯(linear temporal logic，簡(jiǎn)稱LTL)是一種與時(shí)間有關(guān)的模態(tài)時(shí)序邏輯。引入LTL公式來(lái)描述系統(tǒng)行為屬性，通過(guò)使用原子命題、析取操作符(∨)、next算子(X)、until算子(U)和否定操作符號(hào)()定義LTL公式的集合。

定義2(LTL語(yǔ)義) 令u=u0u1…∈Σω是一個(gè)無(wú)限狀態(tài)序列，且Σ=2P，u滿足LTL公式φ，當(dāng)且僅當(dāng)uφ，LTL公式的語(yǔ)義定義為：

utrue；

up，當(dāng)且僅當(dāng)p∈u；

uφ，當(dāng)且僅當(dāng)u/φ；

uφ1∨φ2，當(dāng)且僅當(dāng)uφ1或者uφ2；

uφ1∧φ2，當(dāng)且僅當(dāng)uφ1且uφ2；

uXφ，當(dāng)且僅當(dāng)ui+1φ；

uφ1Uφ2，當(dāng)且僅當(dāng)?k≥0,ukuk+1…φ2和?0≤i

使用這些定義能夠推導(dǎo)出eventually算子(F)、always算子(G)和release算子(R)：Fφ等價(jià)于trueUφ；Gφ等價(jià)于Fφ；φ1Rφ2等價(jià)于(φ1Uφ2)。

1.2 Büchi自動(dòng)機(jī)

Büchi自動(dòng)機(jī)是ω自動(dòng)機(jī)的一種，它將有限狀態(tài)自動(dòng)機(jī)擴(kuò)展到無(wú)限，接受一個(gè)無(wú)限的輸入序列，可以替代和處理ω正則語(yǔ)言。由于Büchi自動(dòng)機(jī)在布爾操作[12]下是封閉的，它常被用于基于自動(dòng)機(jī)的形式化驗(yàn)證方法。

定義3(Büchi自動(dòng)機(jī)) Büchi自動(dòng)機(jī)是一個(gè)五元組B=(Σ,Q,I,δ,F)。其中：Σ為非空有限字母表，且Σ′?2Σ；δ?Q×2Σ′×Q是遷移關(guān)系；Q為非空有限狀態(tài)集合；I?Q為初始狀態(tài)集合；F?Q為接受狀態(tài)集合。

1.3JavaMOP

JavaMOP是一種基于Java語(yǔ)言、支持軟件開(kāi)發(fā)與分析的運(yùn)行時(shí)驗(yàn)證工具，它支持多種邏輯，如線性時(shí)態(tài)邏輯(LTL)、上下無(wú)關(guān)文法(CFG)、擴(kuò)展正則表達(dá)式(ERE)等，并將形式化規(guī)約以邏輯插件的形式集成在JavaMOP工具中，實(shí)現(xiàn)對(duì)不同形式化規(guī)約的監(jiān)控。其中，LTL插件用于驗(yàn)證軟件系統(tǒng)運(yùn)行時(shí)是否滿足給定的LTL屬性。JavaMOP是目前最高效的運(yùn)行時(shí)驗(yàn)證工具之一，在軟件運(yùn)行時(shí)驗(yàn)證中，將LTL語(yǔ)言描述的屬性轉(zhuǎn)換成監(jiān)控器代碼插裝到待監(jiān)控的系統(tǒng)程序中，實(shí)現(xiàn)實(shí)時(shí)監(jiān)控系統(tǒng)程序的運(yùn)行并返回監(jiān)控結(jié)果。JavaMOP運(yùn)行時(shí)監(jiān)控軟件系統(tǒng)程序的過(guò)程如圖1所示。

圖1 JavaMOP運(yùn)行時(shí)監(jiān)控軟件系統(tǒng)程序的過(guò)程

JavaMOP在驗(yàn)證軟件系統(tǒng)時(shí)，根據(jù)給定的屬性規(guī)約會(huì)自動(dòng)生成相應(yīng)的監(jiān)控器代碼，并插裝到目標(biāo)程序中進(jìn)行實(shí)時(shí)監(jiān)控。JavaMOP生成監(jiān)控器基于自動(dòng)機(jī)的驗(yàn)證算法，對(duì)于給定的LTL屬性，通過(guò)轉(zhuǎn)換算法[13]將LTL公式轉(zhuǎn)化為Büchi自動(dòng)機(jī)，再將Büchi自動(dòng)機(jī)轉(zhuǎn)化為確定性有限自動(dòng)機(jī)(determine finite automata，簡(jiǎn)稱DFA)，生成監(jiān)控器的抽象表示，之后得到監(jiān)控器代碼，實(shí)現(xiàn)對(duì)軟件系統(tǒng)程序驗(yàn)證的功能。

2 自動(dòng)機(jī)化簡(jiǎn)規(guī)則與算法

在生成監(jiān)控器的過(guò)程中，減小Büchi自動(dòng)機(jī)的大小，能夠減少內(nèi)存消耗并加快監(jiān)控器代碼的生成。為此，提出自動(dòng)機(jī)化簡(jiǎn)規(guī)則對(duì)由LTL公式轉(zhuǎn)化得到的Büchi自動(dòng)機(jī)進(jìn)行化簡(jiǎn)。首先對(duì)自動(dòng)機(jī)中接受語(yǔ)言為空的狀態(tài)進(jìn)行移除操作；再將滿足合并規(guī)則的狀態(tài)進(jìn)行合并化簡(jiǎn)，使得目標(biāo)Büchi自動(dòng)機(jī)最小化。

規(guī)則1(移除規(guī)則) 設(shè)Büchi自動(dòng)機(jī)B=(Σ,Q,I,δ,F)，對(duì)自動(dòng)機(jī)中的任一狀態(tài)q，若從狀態(tài)q開(kāi)始的自動(dòng)機(jī)接受語(yǔ)言為空，則狀態(tài)q為冗余狀態(tài)可移除。

規(guī)則1即取自動(dòng)機(jī)中的任意一個(gè)狀態(tài)，判斷Büchi自動(dòng)機(jī)接受的語(yǔ)言是否為空，若接受的語(yǔ)言為空，則進(jìn)行冗余標(biāo)記，并移除操作將其刪除。移除冗余算法描述如下。

算法1RemoveRedundant(B)

輸入：Büchi自動(dòng)機(jī)B=(Σ,Q,I,δ,F)；

輸出：新的Büchi自動(dòng)機(jī)B′=(Σ′,Q′,I′,δ′,F′)，且有L(B′)=L(B)。

1 fors∈Qdo；

2 計(jì)算從狀態(tài)s出發(fā)的后繼狀態(tài)集合nodes(s)；

3 if nodes(s)∩F=? then//狀態(tài)s開(kāi)始的自動(dòng)機(jī)語(yǔ)言為空；

4 標(biāo)記狀態(tài)s為冗余狀態(tài)；

5 移除狀態(tài)s；

6 返回Büchi自動(dòng)機(jī)B′。

規(guī)則2(合并規(guī)則) 設(shè)Büchi自動(dòng)機(jī)中狀態(tài)a和狀態(tài)b都有n條遷移關(guān)系，若狀態(tài)a的下一個(gè)狀態(tài)是b,且狀態(tài)a遷移到狀態(tài)b的條件也是狀態(tài)b的自旋條件，同時(shí)狀態(tài)a剩下n-1條遷移與狀態(tài)b的另外n-1遷移相同，則狀態(tài)a和狀態(tài)b可以合并。

合并規(guī)則對(duì)自動(dòng)機(jī)冗余刪除后進(jìn)一步化簡(jiǎn)自動(dòng)機(jī)，用于得到狀態(tài)數(shù)更少的自動(dòng)機(jī)。首先將自動(dòng)機(jī)中的狀態(tài)集分為2個(gè)集合S1和S2，集合S1用于存儲(chǔ)接受狀態(tài)，集合S2存儲(chǔ)除了接受狀態(tài)的自動(dòng)機(jī)狀態(tài)；然后分別對(duì)集合S1和集合S2中的狀態(tài)s和s′進(jìn)行判斷，是否符合合并規(guī)則；若滿足，則可將狀態(tài)s′合并到狀態(tài)s，狀態(tài)s′的環(huán)移動(dòng)到狀態(tài)s。具體執(zhí)行過(guò)程如下。

算法2Merge(B)

輸入：Büchi自動(dòng)機(jī)B′=(Σ′,Q′,I′,δ′,F′)；

輸出：新的Büchi自動(dòng)機(jī)B″=(Σ″,Q″,I″,δ″,F″)，且有L(B″)=L(B′)。

1 fors∈Qdo；

2 ifs∈Fthen；

3S1:=S1∪s//把s加入到接受狀態(tài)集合S1中；

4 else；

5S2:=S2∪s//把s加入到非接受狀態(tài)集合S2中；

6 //對(duì)S1集合中狀態(tài)進(jìn)行合并操作；

7 fors∈S1do；

8 fors′∈S1do；

9 ifs,s′滿足合并規(guī)則 then；

10 合并狀態(tài)s和狀態(tài)s′；

11 //對(duì)S2集合中狀態(tài)進(jìn)行合并操作；

12 fors∈S2do；

13 fors′∈S2do；

14 ifs，s′滿足合并規(guī)則then；

15 合并狀態(tài)s和狀態(tài)s′；

16 返回Büchi自動(dòng)機(jī)B″。

圖2為運(yùn)用合并規(guī)則化簡(jiǎn)自動(dòng)機(jī)狀態(tài)的例子。使用一個(gè)三元組δ表示2個(gè)狀態(tài)之間的遷移關(guān)系，如δ=(s1,c,s2)表示從狀態(tài)s1遷移到狀態(tài)s2的條件是c。圖2(a)為化簡(jiǎn)之前的自動(dòng)機(jī)，它有6個(gè)狀態(tài)和13條遷移關(guān)系，其中狀態(tài)s0有3條遷移關(guān)系δ1=(s0,a,s1)，δ2=(s0,c,s2)，δ3=(s0,b,s3)。狀態(tài)s1也有3條遷移關(guān)系δ4=(s1,a,s1)，δ5=(s1,c,s2)，δ6=(s1,b,s3)。狀態(tài)s0遷移到狀態(tài)s1與狀態(tài)s1到自身的條件相同，并且剩下的2條遷移也相同，因此，狀態(tài)s0和s1滿足合并規(guī)則，可將s0與s1合并。同樣地，狀態(tài)s3和s4滿足合并規(guī)則，可以合并。化簡(jiǎn)得到新的自動(dòng)機(jī)如圖2(b)所示，它包含4個(gè)狀態(tài)和7條遷移關(guān)系，與化簡(jiǎn)前相比簡(jiǎn)單了很多。

圖2 運(yùn)用合并規(guī)則化簡(jiǎn)自動(dòng)機(jī)的例子

3 實(shí)驗(yàn)與分析

為了驗(yàn)證自動(dòng)機(jī)化簡(jiǎn)規(guī)則的可行性，用Java語(yǔ)言實(shí)現(xiàn)了基于自動(dòng)機(jī)的監(jiān)控器構(gòu)造過(guò)程，并與JavaMOP中原有構(gòu)造運(yùn)行時(shí)監(jiān)控器的方法進(jìn)行比較。為了使2種監(jiān)控器構(gòu)造方法的實(shí)驗(yàn)數(shù)據(jù)具有可比性和公平性，采用相同的測(cè)試用例，所有實(shí)驗(yàn)在相同的環(huán)境下進(jìn)行。實(shí)驗(yàn)運(yùn)行環(huán)境的配置如下：處理器為Inter (R) Core (TM) i5-4690 CPU@3.5 GHz和內(nèi)存為8 GiB的臺(tái)式電腦，電腦配備的操作系統(tǒng)為Ubuntu 14.04，同時(shí)配置了Sun Java SE 8環(huán)境。使用DaCapo[14]數(shù)據(jù)集，選取其中4個(gè)測(cè)試屬性作為實(shí)驗(yàn)的測(cè)試對(duì)象，分別為：

HasNext：對(duì)于每個(gè)迭代器對(duì)象，要求在執(zhí)行函數(shù)next()前調(diào)用函數(shù)hasnext()，并且hasnext()的返回值為true；

SafeSyncColl：若一個(gè)集合是同步的，則它的迭代器也應(yīng)是同步訪問(wèn)的；

UnSafeIterator：在使用迭代器接口迭代集合元素時(shí)不能更新集合元素；

UnSafeMapIterator：在集合上對(duì)映射的鍵值迭代時(shí)，Map無(wú)法進(jìn)行更新操作。

表1為2種監(jiān)控器構(gòu)造方法的性能比較。從表1可看出，在內(nèi)存開(kāi)銷方面，化簡(jiǎn)Büchi自動(dòng)機(jī)能夠減少運(yùn)行時(shí)監(jiān)控器在構(gòu)造過(guò)程中的內(nèi)存消耗；在時(shí)間開(kāi)銷上，簡(jiǎn)化的Büchi自動(dòng)機(jī)加速了生成監(jiān)控器的過(guò)程，從而節(jié)省了構(gòu)造監(jiān)控器代碼的時(shí)間，降低了整個(gè)監(jiān)控器構(gòu)造的時(shí)間開(kāi)銷。對(duì)于測(cè)試的屬性HasNext，化簡(jiǎn)操作前JavaMop時(shí)間和內(nèi)存開(kāi)銷分別為92.88 s和629.71 MiB，本方法時(shí)間和內(nèi)存開(kāi)銷分別為89.92 s和612.23 MiB，在時(shí)間和內(nèi)存開(kāi)銷分別降低了3.19%和2.78%。對(duì)于屬性UnSafeIterator，本方法時(shí)間和內(nèi)存開(kāi)銷分別降低4.93%和5.32%，比屬性HasNext性能提升更多，這是因?yàn)閷傩訳nSafeIterator操作更加復(fù)雜，經(jīng)過(guò)化簡(jiǎn)操作后移除和約減的狀態(tài)和遷移關(guān)系更多，因此，性能提升也相對(duì)更多。

表1 2種監(jiān)控器構(gòu)造方法的性能比較

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

對(duì)于運(yùn)行時(shí)驗(yàn)證中基于自動(dòng)機(jī)理論構(gòu)造監(jiān)控器的方法，通過(guò)化簡(jiǎn)Büchi自動(dòng)機(jī)來(lái)減小運(yùn)行時(shí)驗(yàn)證在監(jiān)控器構(gòu)造過(guò)程中的時(shí)間和內(nèi)存開(kāi)銷，能夠提高監(jiān)控器生成的效率和運(yùn)行時(shí)驗(yàn)證的性能。針對(duì)運(yùn)行時(shí)驗(yàn)證工具JavaMOP中構(gòu)造監(jiān)控器的方法進(jìn)行研究實(shí)驗(yàn)，實(shí)驗(yàn)結(jié)果表明，本方法在提升運(yùn)行時(shí)監(jiān)控性能上有一定的效果。今后研究監(jiān)控器代碼生成后對(duì)程序進(jìn)行實(shí)時(shí)監(jiān)控過(guò)程中監(jiān)控算法的優(yōu)化，提高監(jiān)控算法效率，以進(jìn)一步降低運(yùn)行時(shí)驗(yàn)證的時(shí)間和內(nèi)存開(kāi)銷。